import GinibrePoincare.Concrete.NormalizedGroundState
import GinibrePoincare.Concrete.SmoothTarget
import GinibrePoincare.Concrete.Wirtinger

/-!
# Holomorphic distance on the Ginibre side

The main proof compares the Gaussian distance to alternating holomorphic
functions with the Ginibre distance to symmetric entire functions.  The
quantities are defined here directly on representatives.
-/

open MeasureTheory

namespace GinibrePoincare

noncomputable section

/-- Square-integrability of a complex function for the Ginibre measure. -/
def IsGinibreL2 (n : ℕ) (h : Configuration n → ℂ) : Prop :=
  Integrable (fun z => Complex.normSq (h z)) (ginibreMeasure n)

/-- Symmetric entire square-integrable functions on the Ginibre space. -/
def IsSymmetricEntireL2 {n : ℕ}
    (h : Configuration n → ℂ) : Prop :=
  IsSymmetric h ∧ IsEntire h ∧ IsGinibreL2 n h

/-- Squared Ginibre `L²` error from a real observable to a complex function. -/
def ginibreComplexError (n : ℕ) (f : Configuration n → ℝ)
    (h : Configuration n → ℂ) : ℝ :=
  ∫ z, Complex.normSq ((f z : ℂ) - h z) ∂ginibreMeasure n

/-- Errors of symmetric entire Ginibre approximants. -/
def ginibreHolomorphicErrors (n : ℕ)
    (f : Configuration n → ℝ) : Set ℝ :=
  {r | ∃ h : Configuration n → ℂ,
    IsSymmetricEntireL2 h ∧ r = ginibreComplexError n f h}

/-- Squared distance to the symmetric entire Ginibre subspace. -/
def ginibreHolomorphicDistanceSq (n : ℕ)
    (f : Configuration n → ℝ) : ℝ :=
  sInf (ginibreHolomorphicErrors n f)

/-- Centering of a real observable. -/
def centeredObservable (n : ℕ) (f : Configuration n → ℝ) :
    Configuration n → ℝ :=
  fun z => f z - smoothGinibreMean n f

/-- Distance identity required from the isometry and holomorphic divisibility. -/
def GroundStateDistanceIdentityStatement : Prop :=
  ∀ n : ℕ, 0 < n →
    IsProbabilityMeasure (ginibreMeasure n) →
    ∀ f : Configuration n → ℝ,
      IsSmoothCompactSymmetric f →
      gaussianHolomorphicDistanceSq n
          (normalizedVandermondeTransform n
            (fun z => (centeredObservable n f z : ℂ))) =
        ginibreHolomorphicDistanceSq n (centeredObservable n f)

/-- Half-distance estimate supplied by the real projection geometry. -/
def GinibreHalfDistanceStatement : Prop :=
  ∀ n : ℕ, 0 < n →
    IsProbabilityMeasure (ginibreMeasure n) →
    ∀ f : Configuration n → ℝ,
      IsSmoothCompactSymmetric f →
      smoothGinibreVariance n f / 2 ≤
        ginibreHolomorphicDistanceSq n (centeredObservable n f)

end

end GinibrePoincare