DimdPoly

Showcase: stable phase recovery for Hermite-Fock expansions

This file is the explained, proved public version of the qualitative fixed-dimension phase-retrieval theorem.

The public statement deliberately uses only ordinary Mathlib objects:

• a point is a vector z : Fin d -> ℂ;
• a finite signal is a finitely supported coefficient array F : Finsupp (Fin d -> ℕ) ℂ;
• the basis functions are written out as explicit finite products of explicit one-variable complex Hermite polynomials;
• TrueHermitePoly κ F is the finite linear combination ∑ α, F α * Φ κ α;
• TrueHermitePolys κ is the set of all functions that arise this way;
• TrueHermiteFunctions κ is the Gaussian L^2 closure of those finite functions;
• the stability defect is an explicit Gaussian L^2 norm of a difference of measured magnitudes.

The theorem stable_phase_retrieval is the main qualitative statement: it keeps the reference signal P finite, but allows the comparison signal Q to lie in the Gaussian L^2 closure of TrueHermitePolys κ.

Explicit Hermite-Fock basis

noncomputable def DimdPolyShowcaseChallenge.HermitePoly (k n : ℕ) (z : ℂ) : ℂ

The normalized one-variable Hermite-Fock basis polynomial.

The fixed index k is the Hermite level, while n is the coefficient index.

Lean's Finset.range N is the finite set {0, ..., N - 1}. Thus Finset.range (min n k + 1) indexes exactly j = 0, ..., min n k, matching the inclusive upper limit in the paper formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DimdPolyShowcaseChallenge.Φ {d : ℕ} (κ α : Fin d → ℕ) (z : Fin d → ℂ) : ℂ

The d-variable basis element.

For each coordinate q, take the one-variable basis polynomial determined by κ q and α q, then multiply the results over all coordinates.

Equations

• DimdPolyShowcaseChallenge.Φ κ α z = ∏ q : Fin d, DimdPolyShowcaseChallenge.HermitePoly (κ q) (α q) (z q)

noncomputable def DimdPolyShowcaseChallenge.TrueHermitePoly {d : ℕ} (κ : Fin d → ℕ) (F : (Fin d → ℕ) →₀ ℂ) : (Fin d → ℂ) → ℂ

The finite Hermite-Fock polynomial attached to a finite coefficient array.

This is the reader-friendly finite model: it is just a finite sum of explicit basis polynomials with complex coefficients.

Equations

• DimdPolyShowcaseChallenge.TrueHermitePoly κ F z = F.sum fun (α : Fin d → ℕ) (c : ℂ) => c * DimdPolyShowcaseChallenge.Φ κ α z

def DimdPolyShowcaseChallenge.TrueHermitePolys {d : ℕ} (κ : Fin d → ℕ) : Set ((Fin d → ℂ) → ℂ)

The set of all finite Hermite-Fock polynomials at level κ.

This is just the range of the explicit coefficient formula above. Thus a function P belongs to TrueHermitePolys κ exactly when it can be written as TrueHermitePoly κ F for some finite coefficient array F.

Equations

• DimdPolyShowcaseChallenge.TrueHermitePolys κ = Set.range (DimdPolyShowcaseChallenge.TrueHermitePoly κ)

Gaussian measure and coefficient geometry

noncomputable def DimdPolyShowcaseChallenge.gaussianDensity {d : ℕ} (z : Fin d → ℂ) : ℝ

The real-valued Gaussian density on Fin d -> ℂ.

Equations

• DimdPolyShowcaseChallenge.gaussianDensity z = 1 / Real.pi ^ d * Real.exp (-∑ q : Fin d, ‖z q‖ ^ 2)

noncomputable def DimdPolyShowcaseChallenge.γ {d : ℕ} : MeasureTheory.Measure (Fin d → ℂ)

The product Gaussian measure on Fin d -> ℂ.

Equations

• DimdPolyShowcaseChallenge.γ = MeasureTheory.volume.withDensity fun (z : Fin d → ℂ) => ENNReal.ofReal (DimdPolyShowcaseChallenge.gaussianDensity z)

def DimdPolyShowcaseChallenge.TrueHermiteFunctions {d : ℕ} (κ : Fin d → ℕ) : Set ↥(MeasureTheory.Lp ℂ 2 γ)

The Gaussian L² closure of finite Hermite-Fock polynomials at level κ. Note that functions in L² are only defined up to almost-everywhere equality, and come with integrability guarantees so we use f =ᵐ[γ] P to denote this "equal in measure" statement.

Equations

• One or more equations did not get rendered due to their size.

theorem DimdPolyShowcaseChallenge.stable_phase_retrieval {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ TrueHermitePolys κ) : ∃ (M : ℝ), 0 < M ∧ ∀ Q ∈ TrueHermiteFunctions κ, ∃ (θ : ℂ), ‖θ‖ = 1 ∧ ∫ (z : Fin d → ℂ), ‖P z - θ * ↑↑Q z‖ ^ 2 ∂γ ≤ M ^ 2 * ∫ (z : Fin d → ℂ), (‖P z‖ - ‖↑↑Q z‖) ^ 2 ∂γ

Stable phase retrieval for Gaussian L² limits of finite Hermite-Fock polynomials.

This is the main qualitative statement. The comparison signal Q is an element of the Gaussian L² closure of the finite Hermite-Fock polynomials.