Auxiliary

Auxiliary bridge for the showcase theorem

This file keeps the coefficient-level normalization and rescaling argument out of DimdPoly.lean. The public file deliberately restates the public definitions; the lemmas here use equivalent explicit objects so the public file can unfold only paper-facing definitions.

noncomputable def DimdPolyLEAN.explicitGaussianDensity (d : ℕ) (z : Fin d → ℂ) : ℝ

explicitGaussianDensity: explicit Gaussian Density.

Equations

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

noncomputable def DimdPolyLEAN.explicitGamma (d : ℕ) : MeasureTheory.Measure (Fin d → ℂ)

explicitGamma: explicit Gamma.

Equations

• DimdPolyLEAN.explicitGamma d = MeasureTheory.volume.withDensity fun (z : Fin d → ℂ) => ENNReal.ofReal (DimdPolyLEAN.explicitGaussianDensity d z)

def DimdPolyLEAN.explicitComplexHermite (m n : ℕ) (z : ℂ) : ℂ

explicitComplexHermite: explicit Complex Hermite.

Equations

• DimdPolyLEAN.explicitComplexHermite m n z = ∑ j ∈ Finset.range (min m n + 1), (-1) ^ j * ↑j.factorial * ↑(m.choose j) * ↑(n.choose j) * z ^ (m - j) * star z ^ (n - j)

noncomputable def DimdPolyLEAN.explicitPhi1D (k n : ℕ) (z : ℂ) : ℂ

explicitPhi1D: explicit Phi1 D.

Equations

• DimdPolyLEAN.explicitPhi1D k n z = (↑√(↑n.factorial * ↑k.factorial))⁻¹ * DimdPolyLEAN.explicitComplexHermite n k z

noncomputable def DimdPolyLEAN.explicitPhi {d : ℕ} (kappa alpha : Fin d → ℕ) (z : Fin d → ℂ) : ℂ

explicitPhi: explicit Phi.

Equations

• DimdPolyLEAN.explicitPhi kappa alpha z = ∏ q : Fin d, DimdPolyLEAN.explicitPhi1D (kappa q) (alpha q) (z q)

noncomputable def DimdPolyLEAN.explicitPkappaNorm {d : ℕ} (F : (Fin d → ℕ) →₀ ℂ) : ℝ

explicitPkappaNorm: explicit Pkappa Norm.

Equations

• DimdPolyLEAN.explicitPkappaNorm F = √(∑ alpha ∈ F.support, ‖F alpha‖ ^ 2)

noncomputable def DimdPolyLEAN.explicitEvalPkappa {d : ℕ} (kappa : Fin d → ℕ) (F : (Fin d → ℕ) →₀ ℂ) : (Fin d → ℂ) → ℂ

explicitEvalPkappa: explicit Eval Pkappa.

Equations

• DimdPolyLEAN.explicitEvalPkappa kappa F z = F.sum fun (alpha : Fin d → ℕ) (c : ℂ) => c * DimdPolyLEAN.explicitPhi kappa alpha z

theorem DimdPolyLEAN.stablePhaseRetrievalCoefficients {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (F : (Fin d → ℕ) →₀ ℂ) (hF : F ≠ 0) : ∃ (C_F : ℝ), 0 < C_F ∧ ∀ (Q : (Fin d → ℕ) →₀ ℂ), ∃ (θ : ℂ), ‖θ‖ = 1 ∧ ∫ (z : Fin d → ℂ), ‖explicitEvalPkappa κ F z - θ * explicitEvalPkappa κ Q z‖ ^ 2 ∂explicitGamma d ≤ C_F ^ 2 * ∫ (z : Fin d → ℂ), (‖explicitEvalPkappa κ F z‖ - ‖explicitEvalPkappa κ Q z‖) ^ 2 ∂explicitGamma d

theorem DimdPolyLEAN.stablePhaseRetrievalCoefficientsAll {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (F : (Fin d → ℕ) →₀ ℂ) : ∃ (C_F : ℝ), 0 < C_F ∧ ∀ (Q : (Fin d → ℕ) →₀ ℂ), ∃ (θ : ℂ), ‖θ‖ = 1 ∧ ∫ (z : Fin d → ℂ), ‖explicitEvalPkappa κ F z - θ * explicitEvalPkappa κ Q z‖ ^ 2 ∂explicitGamma d ≤ C_F ^ 2 * ∫ (z : Fin d → ℂ), (‖explicitEvalPkappa κ F z‖ - ‖explicitEvalPkappa κ Q z‖) ^ 2 ∂explicitGamma d

theorem DimdPolyLEAN.stablePhaseRetrievalExplicitRange {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ Set.range (explicitEvalPkappa κ)) : ∃ (C_P : ℝ), 0 < C_P ∧ ∀ Q ∈ Set.range (explicitEvalPkappa κ), ∃ (θ : ℂ), ‖θ‖ = 1 ∧ ∫ (z : Fin d → ℂ), ‖P z - θ * Q z‖ ^ 2 ∂explicitGamma d ≤ C_P ^ 2 * ∫ (z : Fin d → ℂ), (‖P z‖ - ‖Q z‖) ^ 2 ∂explicitGamma d

Closure upgrade

noncomputable def DimdPolyLEAN.explicitGaussianL2DistanceSq {d : ℕ} (P Q : (Fin d → ℂ) → ℂ) : ℝ

explicitGaussianL2DistanceSq: explicit Gaussian L2 Distance Sq.

Equations

• DimdPolyLEAN.explicitGaussianL2DistanceSq P Q = ∫ (z : Fin d → ℂ), ‖P z - Q z‖ ^ 2 ∂DimdPolyLEAN.explicitGamma d

noncomputable def DimdPolyLEAN.explicitModulusDistanceSq {d : ℕ} (P Q : (Fin d → ℂ) → ℂ) : ℝ

explicitModulusDistanceSq: explicit Modulus Distance Sq.

Equations

• DimdPolyLEAN.explicitModulusDistanceSq P Q = ∫ (z : Fin d → ℂ), (‖P z‖ - ‖Q z‖) ^ 2 ∂DimdPolyLEAN.explicitGamma d

def DimdPolyLEAN.UnitPhase : Type

UnitPhase: Unit Phase.

Equations

• DimdPolyLEAN.UnitPhase = { θ : ℂ // ‖θ‖ = 1 }

@[implicit_reducible]

instance DimdPolyLEAN.instTopologicalSpaceUnitPhase : TopologicalSpace UnitPhase

Equations

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

@[implicit_reducible]

noncomputable instance DimdPolyLEAN.instMetricSpaceUnitPhase : MetricSpace UnitPhase

Equations

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

instance DimdPolyLEAN.instCompactSpaceUnitPhase : CompactSpace UnitPhase

@[implicit_reducible]

instance DimdPolyLEAN.instInhabitedUnitPhase : Inhabited UnitPhase

Equations

• DimdPolyLEAN.instInhabitedUnitPhase = { default := ⟨1, DimdPolyLEAN.instInhabitedUnitPhase._proof_1⟩ }

noncomputable def DimdPolyLEAN.explicitPhaseOptimizedDistanceSq {d : ℕ} (P Q : (Fin d → ℂ) → ℂ) : ℝ

explicitPhaseOptimizedDistanceSq: explicit Phase Optimized Distance Sq.

Equations

• DimdPolyLEAN.explicitPhaseOptimizedDistanceSq P Q = sInf (Set.range fun (θ : DimdPolyLEAN.UnitPhase) => DimdPolyLEAN.explicitGaussianL2DistanceSq P fun (z : Fin d → ℂ) => ↑θ * Q z)

def DimdPolyLEAN.explicitHermiteLpPolys {d : ℕ} (κ : Fin d → ℕ) : Set ↥(MeasureTheory.Lp ℂ 2 (explicitGamma d))

explicitHermiteLpPolys: explicit Hermite Lp Polys.

Equations

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

def DimdPolyLEAN.explicitClosureOfHermitePolys {d : ℕ} (κ : Fin d → ℕ) : Set ((Fin d → ℂ) → ℂ)

explicitClosureOfHermitePolys: explicit Closure Of Hermite Polys.

Equations

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

theorem DimdPolyLEAN.explicitHermitePolys_subset_explicitClosure {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) : Set.range (explicitEvalPkappa κ) ⊆ explicitClosureOfHermitePolys κ

theorem DimdPolyLEAN.stablePhaseRetrievalExplicitClosure {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ Set.range (explicitEvalPkappa κ)) : ∃ (C_P : ℝ), 0 < C_P ∧ ∀ Q ∈ explicitClosureOfHermitePolys κ, explicitPhaseOptimizedDistanceSq P Q ≤ C_P ^ 2 * explicitModulusDistanceSq P Q

theorem DimdPolyLEAN.stablePhaseRetrievalExplicitLpClosure {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ Set.range (explicitEvalPkappa κ)) : ∃ (C_P : ℝ), 0 < C_P ∧ ∀ Q ∈ closure (explicitHermiteLpPolys κ), explicitPhaseOptimizedDistanceSq P ↑↑Q ≤ C_P ^ 2 * explicitModulusDistanceSq P ↑↑Q

theorem DimdPolyLEAN.stablePhaseRetrievalExplicitLpClosure_exists {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ Set.range (explicitEvalPkappa κ)) : ∃ (C_P : ℝ), 0 < C_P ∧ ∀ Q ∈ closure (explicitHermiteLpPolys κ), ∃ (θ : ℂ), ‖θ‖ = 1 ∧ (explicitGaussianL2DistanceSq P fun (z : Fin d → ℂ) => θ * ↑↑Q z) ≤ C_P ^ 2 * explicitModulusDistanceSq P ↑↑Q

theorem DimdPolyLEAN.stablePhaseRetrievalExplicitLpClosure_ae {d : ℕ} (hd : 0 < d) (κ : Fin d → ℕ) (P : (Fin d → ℂ) → ℂ) (hP : P ∈ Set.range (explicitEvalPkappa κ)) : ∃ (C_P : ℝ), 0 < C_P ∧ ∀ Q ∈ closure {f : ↥(MeasureTheory.Lp ℂ 2 (explicitGamma d)) | ∃ P ∈ Set.range (explicitEvalPkappa κ), ↑↑f =ᵐ[explicitGamma d] P}, ∃ (θ : ℂ), ‖θ‖ = 1 ∧ (explicitGaussianL2DistanceSq P fun (z : Fin d → ℂ) => θ * ↑↑Q z) ≤ C_P ^ 2 * explicitModulusDistanceSq P ↑↑Q