ImportedAnalyticInputs

def Hermite1DimdLEAN.oneDimLift (f : ℂ → ℂ) : CSpace 1 → ℂ

oneDimLift: one Dim Lift.

Equations

• Hermite1DimdLEAN.oneDimLift f z = f (z 0)

ImportedAnalyticInputs

Statement-only scaffold for the one-variable and abstract analytic inputs. Scaffolding notes: ScaffoldingNotes/Imported/analytic_inputs.md.

theorem Hermite1DimdLEAN.oneVariableBasisOrthonormal (k m n : ℕ) : gaussianInner (oneDimLift (oneDimPhi k m)) (oneDimLift (oneDimPhi k n)) = if m = n then 1 else 0

Imported one-variable basis orthonormality at fixed true-Hermite level.

theorem Hermite1DimdLEAN.oneVariableFiniteParseval (k : ℕ) (G : FiniteHermiteSum 1) : hermiteNormSq (fun (x : Fin 1) => k) G = ∑ n ∈ G.support, ‖G.coeff n‖ ^ 2

Imported one-variable Parseval statement for finite coefficient families.

theorem Hermite1DimdLEAN.oneVariableLocalization (k : ℕ) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (n j : ℕ), 1 ≤ n → annulusMass (fun (x : Fin 1) => j) (oneDimLift (oneDimPhi k n)) ≤ C * Real.exp (-c * max (|↑j - √↑n| - ↑(k + 4)) 0 ^ 2)

Imported one-variable localization estimate for n ≥ 1.

theorem Hermite1DimdLEAN.positiveFrequencyCircleEstimate (E : Finset ℕ) (b : ℕ → ℂ) (hpos : ∀ n ∈ E, 0 < n) (_hP : HasPositiveFrequencySupport (positiveFrequencyPolynomial E b) E) : circleL2NormSq (positiveFrequencyPolynomial E b) ≤ 144 * ↑E.card * circleL2NormSq fun (t : Circle) => rho 1 (positiveFrequencyPolynomial E b t)

Imported positive-frequency circle estimate with frozen constant 144.

theorem Hermite1DimdLEAN.highFrequencyBandEstimate (N L : ℕ) (c : Fin L → ℂ) (hgap : 1343 * L ^ 2 ≤ N ^ 2) (hP : HasBandlimitedSupport (bandLimitedPolynomial N L c) N L) : circleL2NormSq (bandLimitedPolynomial N L c) ≤ 32 * circleL2NormSq fun (t : Circle) => rho 1 (bandLimitedPolynomial N L c t)

Imported high-frequency band estimate with frozen constants 32 and 1343.

theorem Hermite1DimdLEAN.localizationIncludingZero (k : ℕ) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ∀ (n j : ℕ), annulusMass (fun (x : Fin 1) => j) (oneDimLift (oneDimPhi k n)) ≤ C * Real.exp (-c * max (|↑j - √↑n| - ↑(k + 4)) 0 ^ 2)

Project-owned upgrade of localization that now includes the zero mode.

theorem Hermite1DimdLEAN.scaledPositiveFrequencyCircleEstimate (a : ℂ) (E : Finset ℕ) (P : Circle → ℂ) (hpos : ∀ n ∈ E, 0 < n) (hP : HasPositiveFrequencySupport P E) : circleL2NormSq P ≤ 144 * ↑E.card * circleL2NormSq fun (t : Circle) => rho a (P t)

Scalar-rescaled positive-frequency estimate for an arbitrary background a.

theorem Hermite1DimdLEAN.scaledHighFrequencyBandEstimate (a : ℂ) (N L : ℕ) (P : Circle → ℂ) (hgap : 1343 * L ^ 2 ≤ N ^ 2) (hP : HasBandlimitedSupport P N L) : circleL2NormSq P ≤ 32 * circleL2NormSq fun (t : Circle) => rho a (P t)

Scalar-rescaled high-frequency estimate for an arbitrary background a.

theorem Hermite1DimdLEAN.oneVariableAngularFactorization (k n : ℕ) : ∃ (radial : Polynomial ℝ), ∀ (r t : ℝ), oneDimPhi k n (↑r * Complex.exp (Complex.I * ↑t)) = Complex.exp (Complex.I * ((↑↑n - ↑↑k) * ↑t)) * Polynomial.eval₂ (algebraMap ℝ ℂ) (↑r) radial

theorem Hermite1DimdLEAN.tensorGaussianFactorization (d : ℕ) (F G : Fin d → ℂ → ℂ) (hFG : ∀ (q : Fin d), MeasureTheory.Integrable (fun (z : CSpace 1) => F q (z 0) * (starRingEnd ℂ) (G q (z 0))) (gaussianMeasure 1)) : MeasureTheory.Integrable (fun (z : CSpace d) => ∏ q : Fin d, F q (z q) * (starRingEnd ℂ) (G q (z q))) (gaussianMeasure d) ∧ (gaussianInner (fun (z : CSpace d) => ∏ q : Fin d, F q (z q)) fun (z : CSpace d) => ∏ q : Fin d, G q (z q)) = ∏ q : Fin d, gaussianInner (fun (z : CSpace 1) => F q (z 0)) fun (z : CSpace 1) => G q (z 0)

Tensor-product factorization over the Gaussian product measure.