import GinibrePoincare.Analysis.MultivariateHermiteIntegrability
import GinibrePoincare.Analysis.PolynomialCompactApproximation
import Mathlib.MeasureTheory.Function.ContinuousMapDense

/-! # Polynomial subspaces in Gaussian `L²`

This module packages the multivariate complex Hermite polynomials as actual
vectors of Gaussian `L²`, and records the unconditional analytic density
input supplied by weak regularity: bounded continuous functions are dense in
that space.  This is the natural first reduction in the proof that the
Hermite polynomial span is dense.
-/

open MeasureTheory
open Filter
open scoped ENNReal

namespace GinibrePoincare

noncomputable section

open ComplexHermite

/-- A normalized multivariate complex Hermite polynomial, regarded as a
vector of Gaussian `L²`. -/
def multivariateNormalizedL2 (n : ℕ) (hn : 0 < n)
    (p q : Fin n → ℕ) : Lp ℂ 2 (complexGaussianMeasure n) :=
  (memLp_two_multivariateNormalized n hn p q).toLp
    (multivariateNormalized n hn p q)

theorem multivariateNormalizedL2_coeFn (n : ℕ) (hn : 0 < n)
    (p q : Fin n → ℕ) :
    multivariateNormalizedL2 n hn p q =ᵐ[complexGaussianMeasure n]
      multivariateNormalized n hn p q :=
  (memLp_two_multivariateNormalized n hn p q).coeFn_toLp

/-- The algebraic subspace generated by all multivariate normalized Hermite
polynomials. -/
def gaussianHermiteSpan (n : ℕ) (hn : 0 < n) :
    Submodule ℂ (Lp ℂ 2 (complexGaussianMeasure n)) :=
  Submodule.span ℂ (Set.range fun pq : (Fin n → ℕ) × (Fin n → ℕ) ↦
    multivariateNormalizedL2 n hn pq.1 pq.2)

theorem multivariateNormalizedL2_mem_span (n : ℕ) (hn : 0 < n)
    (p q : Fin n → ℕ) :
    multivariateNormalizedL2 n hn p q ∈ gaussianHermiteSpan n hn := by
  apply Submodule.subset_span
  exact ⟨(p, q), rfl⟩

/-- Bounded continuous functions form an unconditionally dense class in the
finite-dimensional complex Gaussian `L²` space. -/
theorem gaussian_boundedContinuousFunction_dense (n : ℕ) :
    Dense (Lp.boundedContinuousFunction ℂ 2 (complexGaussianMeasure n) :
      Set (Lp ℂ 2 (complexGaussianMeasure n))) := by
  exact Lp.boundedContinuousFunction_dense ℂ (complexGaussianMeasure n)
    (by norm_num)

/-- Equivalently, the continuous map sending a bounded continuous function
to its Gaussian `L²` class has dense range. -/
theorem gaussian_boundedContinuous_toLp_denseRange (n : ℕ) :
    DenseRange (BoundedContinuousFunction.toLp (E := ℂ) 2
      (complexGaussianMeasure n) ℂ) := by
  simpa using (BoundedContinuousFunction.toLp_denseRange
    (p := (2 : ℝ≥0∞)) ℂ (complexGaussianMeasure n) ℂ (by norm_num))

/-- Closed balls exhaust configuration space in Gaussian measure; equivalently
their complements have mass tending to zero.  This is the tail input for the
cutoff step in polynomial approximation. -/
theorem tendsto_complexGaussianMeasure_compl_closedBall (n : ℕ) :
    Tendsto (fun R : ℕ ↦ complexGaussianMeasure n
      (Metric.closedBall (0 : Configuration n) R)ᶜ) atTop (nhds 0) := by
  have hlim : Tendsto (fun R : ℕ ↦ complexGaussianMeasure n
      (Metric.closedBall (0 : Configuration n) R)ᶜ) atTop
      (nhds (complexGaussianMeasure n
        (⋂ R : ℕ, (Metric.closedBall (0 : Configuration n) R)ᶜ))) := by
    refine tendsto_measure_iInter_atTop
      (fun R ↦ measurableSet_closedBall.compl.nullMeasurableSet)
      (fun R S hRS ↦ Set.compl_subset_compl.mpr ?_) ?_
    · exact Metric.closedBall_subset_closedBall (by exact_mod_cast hRS)
    · exact ⟨0, measure_ne_top _ _⟩
  have hinter : (⋂ R : ℕ,
      (Metric.closedBall (0 : Configuration n) R)ᶜ) = ∅ := by
    rw [← Set.compl_iUnion]
    simp
  simpa [hinter] using hlim

theorem exists_complexGaussianMeasure_compl_closedBall_lt (n : ℕ)
    {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ R : ℕ, complexGaussianMeasure n
      (Metric.closedBall (0 : Configuration n) R)ᶜ < ε := by
  have heventually := (tendsto_order.1
    (tendsto_complexGaussianMeasure_compl_closedBall n)).2 ε hε
  exact heventually.exists

end

end GinibrePoincare