PhaseStability

Phase-stable polynomial recovery

This file adds the phase-optimized layer on top of the existing orthogonal coercivity theorem. The proof works inside the concrete polynomial subspace of L²(gammaD d), so the public statement remains about finite coefficient arrays.

noncomputable def DimdPolyLEAN.modulusDefect {d : ℕ} (kappa : MultiIndex d) (F Q : Pkappa d kappa) : ℝ

The Gaussian L² modulus defect between two finite Hermite-Fock polynomials.

Equations

• DimdPolyLEAN.modulusDefect kappa F Q = √(∫ (z : DimdPolyLEAN.Cd d), (‖DimdPolyLEAN.evalPkappa kappa Q z‖ - ‖DimdPolyLEAN.evalPkappa kappa F z‖) ^ 2 ∂DimdPolyLEAN.gammaD d)

noncomputable def DimdPolyLEAN.phasedCoeffDistance {d : ℕ} {kappa : MultiIndex d} (F Q : Pkappa d kappa) (phase : ℂ) : ℝ

The coefficient distance after applying a chosen global phase to Q.

Equations

• DimdPolyLEAN.phasedCoeffDistance F Q phase = ‖phase • Q - F‖

theorem DimdPolyLEAN.pkappaInner_smul_left {d : ℕ} {kappa : MultiIndex d} (c : ℂ) (Q F : Pkappa d kappa) : pkappaInner (c • Q) F = c * pkappaInner Q F

theorem DimdPolyLEAN.exists_phase_positivePhaseGauge {d : ℕ} {kappa : MultiIndex d} (F Q : Pkappa d kappa) : ∃ (phase : ℂ), ‖phase‖ = 1 ∧ positivePhaseGauge F (phase • Q)

def DimdPolyLEAN.polyL2Submodule {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) : Submodule ℂ ↥(L2Tensor d)

The polynomial subspace of the concrete Gaussian L² space.

Equations

• DimdPolyLEAN.polyL2Submodule hd kappa = { carrier := Set.range (DimdPolyLEAN.evalPkappaL2 kappa), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem DimdPolyLEAN.evalPkappa_lpNorm_eq_norm {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : MeasureTheory.lpNorm (evalPkappa kappa F) 2 (gammaD d) = ‖F‖

theorem DimdPolyLEAN.evalPkappaL2_norm {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) : ‖evalPkappaL2 kappa F‖ = ‖F‖

theorem DimdPolyLEAN.evalPkappaL2_sub {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F G : Pkappa d kappa) : evalPkappaL2 kappa (F - G) = evalPkappaL2 kappa F - evalPkappaL2 kappa G

theorem DimdPolyLEAN.inner_evalPkappaL2_eq_star_pkappaInner {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (G F : Pkappa d kappa) : inner ℂ (evalPkappaL2 kappa G) (evalPkappaL2 kappa F) = star (pkappaInner G F)

theorem DimdPolyLEAN.realGaugeLocalStability {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_norm : ‖F‖ = 1) : ∃ (δ : ℝ) (Mloc : ℝ), 0 < δ ∧ 0 < Mloc ∧ ∀ (H : Pkappa d kappa), ‖H‖ ≤ δ → (pkappaInner H F).im = 0 → ‖H‖ ≤ Mloc * defect F H

Local stability after only fixing the real phase gauge.

This is the direct no-orthogonality consequence of OrthogonalCoercivity: small perturbations whose phase has been normalized are controlled by the measured modulus defect.

theorem DimdPolyLEAN.defect_sub_eq_modulusDefect {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F Q : Pkappa d kappa) : defect F (Q - F) = modulusDefect kappa F Q

Rewriting the perturbation defect as the two-signal modulus defect.

theorem DimdPolyLEAN.modulusDefect_phase_smul {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F Q : Pkappa d kappa) {phase : ℂ} (hphase : ‖phase‖ = 1) : modulusDefect kappa F (phase • Q) = modulusDefect kappa F Q

theorem DimdPolyLEAN.positiveGaugeStability {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_norm : ‖F‖ = 1) : ∃ (C_F : ℝ), 0 < C_F ∧ ∀ (Q : Pkappa d kappa), positivePhaseGauge F Q → ‖Q - F‖ ≤ C_F * modulusDefect kappa F Q

Global stable recovery after fixing the positive phase gauge.

Once Q has been rotated so that its coefficient in the F direction is a nonnegative real, no smallness hypothesis is needed: the coefficient error is controlled by the measured modulus defect.

theorem DimdPolyLEAN.phaseStability {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_norm : ‖F‖ = 1) : ∃ (C_F : ℝ), 0 < C_F ∧ ∀ (Q : Pkappa d kappa), ∃ (phase : ℂ), ‖phase‖ = 1 ∧ phasedCoeffDistance F Q phase ≤ C_F * modulusDefect kappa F Q

Global phase-optimized stability for finite Hermite-Fock polynomials.

For every finite signal Q, one can choose a unit global phase so that the phase-corrected coefficient distance to the normalized base point F is controlled by the measured modulus defect. There is no local δ hypothesis.

theorem DimdPolyLEAN.localPhaseStability {d : ℕ} (hd : 0 < d) (kappa : MultiIndex d) (F : Pkappa d kappa) (hF_norm : ‖F‖ = 1) : ∃ (δ : ℝ) (Mloc : ℝ), 0 < δ ∧ 0 < Mloc ∧ ∀ (Q : Pkappa d kappa), ‖Q - F‖ ≤ δ → ∃ (phase : ℂ), ‖phase‖ = 1 ∧ phasedCoeffDistance F Q phase ≤ Mloc * modulusDefect kappa F Q

Local phase-optimized stability for finite Hermite-Fock polynomials.

Near a normalized nonzero base point F, every nearby finite polynomial Q has a global phase making its coefficients close to those of F, with the distance controlled by the measured modulus defect.