Definitions

noncomputable def HermiteLEAN.T : ℝ

The circle period used throughout the Hermite development.

Equations

• HermiteLEAN.T = 2 * Real.pi

theorem HermiteLEAN.T_pos : 0 < T

instance HermiteLEAN.instFactLtRealOfNatT : Fact (0 < T)

@[reducible, inline]

abbrev HermiteLEAN.Circle : Type

The normalized circle used for Fourier analysis.

Equations

• HermiteLEAN.Circle = AddCircle HermiteLEAN.T

def HermiteLEAN.posPart (x : ℝ) : ℝ

Positive part.

Equations

• HermiteLEAN.posPart x = max x 0

noncomputable def HermiteLEAN.rho (w : ℂ) : ℝ

The signed modulus defect imported from the Fock-space argument.

Equations

• HermiteLEAN.rho w = |‖1 + w‖ - 1|

def HermiteLEAN.phi0 (z : ℂ) : ℂ

The distinguished basis vector Φ₀(z) = \bar z.

Equations

• HermiteLEAN.phi0 z = (starRingEnd ℂ) z

noncomputable def HermiteLEAN.phi : ℕ → ℂ → ℂ

The first true-level Hermite basis vector Φₙ.

We index from 0, with phi 0 = Phi_0 and for n ≥ 1

phi n z = z^(n-1) * (|z|² - n) / sqrt(n!).

Equations

• HermiteLEAN.phi 0 = HermiteLEAN.phi0
• HermiteLEAN.phi n.succ = fun (z : ℂ) => z ^ n * ((↑‖z‖ ^ 2 - ↑↑n.succ) / ↑√↑n.succ.factorial)

noncomputable def HermiteLEAN.weightedInner (F G : ℂ → ℂ) : ℂ

The weighted inner product on L²_γ(ℂ).

Equations

• HermiteLEAN.weightedInner F G = 1 / ↑Real.pi * ∫ (z : ℂ), F z * (starRingEnd ℂ) (G z) * ↑(Real.exp (-‖z‖ ^ 2))

noncomputable def HermiteLEAN.weightedNormSq (F : ℂ → ℂ) : ℝ

The weighted squared norm on L²_γ(ℂ).

Equations

• HermiteLEAN.weightedNormSq F = 1 / Real.pi * ∫ (z : ℂ), ‖F z‖ ^ 2 * Real.exp (-‖z‖ ^ 2)

noncomputable def HermiteLEAN.weightedNorm (F : ℂ → ℂ) : ℝ

The weighted norm on L²_γ(ℂ).

Equations

• HermiteLEAN.weightedNorm F = √(HermiteLEAN.weightedNormSq F)

noncomputable def HermiteLEAN.modulusDefect (F0 G : ℂ → ℂ) (z : ℂ) : ℝ

The pointwise modulus defect relative to a background function F₀.

Equations

• HermiteLEAN.modulusDefect F0 G z = |‖F0 z + G z‖ - ‖F0 z‖|

noncomputable def HermiteLEAN.weightedDefectNormSq (F0 G : ℂ → ℂ) : ℝ

The weighted squared defect norm relative to a background function F₀.

Equations

• HermiteLEAN.weightedDefectNormSq F0 G = 1 / Real.pi * ∫ (z : ℂ), HermiteLEAN.modulusDefect F0 G z ^ 2 * Real.exp (-‖z‖ ^ 2)

noncomputable def HermiteLEAN.weightedDefectNorm (F0 G : ℂ → ℂ) : ℝ

The weighted defect norm relative to a background function F₀.

Equations

• HermiteLEAN.weightedDefectNorm F0 G = √(HermiteLEAN.weightedDefectNormSq F0 G)

def HermiteLEAN.Phi0Perp : Set (ℂ → ℂ)

The orthogonal complement to Φ₀, expressed via the weighted inner product.

Equations

• HermiteLEAN.Phi0Perp = {F : ℂ → ℂ | HermiteLEAN.weightedInner F HermiteLEAN.phi0 = 0}

noncomputable def HermiteLEAN.hermiteSum {D : ℕ} (a : Fin D → ℂ) (z : ℂ) : ℂ

A finite orthogonal Hermite perturbation G_a = ∑ a_n Φ_{n+1}.

Equations

• HermiteLEAN.hermiteSum a z = ∑ n : Fin D, a n * HermiteLEAN.phi (↑n + 1) z

noncomputable def HermiteLEAN.hermiteCoeffNormSq {D : ℕ} (a : Fin D → ℂ) : ℝ

The coefficient-side squared norm for a finite Hermite perturbation.

Equations

• HermiteLEAN.hermiteCoeffNormSq a = ∑ n : Fin D, ‖a n‖ ^ 2

noncomputable def HermiteLEAN.circlePoint (r : ℝ) (t : Circle) : ℂ

The unit circle point of radius r and argument t.

Equations

• HermiteLEAN.circlePoint r t = ↑r * (fourier 1) t

noncomputable def HermiteLEAN.circleCoeff {D : ℕ} (a : Fin D → ℂ) (r : ℝ) (n : Fin D) : ℂ

The coefficient appearing in the circle reduction for Φ_{n+1}.

This formula is only intended for r > 0; the radius-zero case is handled separately later on.

Equations

• HermiteLEAN.circleCoeff a r n = a n * ↑(r ^ ↑n * (r ^ 2 - ↑(↑n + 1)) / (r * √↑(↑n + 1).factorial))

noncomputable def HermiteLEAN.circlePolynomial {D : ℕ} (a : Fin D → ℂ) (r : ℝ) : Circle → ℂ

The positive-frequency trigonometric polynomial on the circle attached to G_a.

Equations

• HermiteLEAN.circlePolynomial a r t = ∑ n : Fin D, HermiteLEAN.circleCoeff a r n * (fourier ↑(↑n + 1)) t

noncomputable def HermiteLEAN.positiveTrigonometricPolynomial (E : Finset ℕ) (c : ℕ → ℂ) : Circle → ℂ

A generic positive-frequency trigonometric polynomial.

Equations

• HermiteLEAN.positiveTrigonometricPolynomial E c t = ∑ n ∈ E, c n * (fourier ↑n) t

def HermiteLEAN.frequencyBand (N L : ℕ) : Finset ℕ

Consecutive positive frequencies [N, N + L - 1].

Equations

• HermiteLEAN.frequencyBand N L = Finset.Icc N (N + L - 1)

noncomputable def HermiteLEAN.circleL2Sq (f : Circle → ℂ) : ℝ

The circle L² norm squared with respect to normalized Haar measure.

Equations

• HermiteLEAN.circleL2Sq f = ∫ (t : AddCircle HermiteLEAN.T), ‖f t‖ ^ 2 ∂AddCircle.haarAddCircle

noncomputable def HermiteLEAN.circleRhoNormSq (f : Circle → ℂ) : ℝ

The circle defect against the constant 1.

Equations

• HermiteLEAN.circleRhoNormSq f = ∫ (t : AddCircle HermiteLEAN.T), HermiteLEAN.rho (f t) ^ 2 ∂AddCircle.haarAddCircle

noncomputable def HermiteLEAN.circleModulusDefect (F0 G : Circle → ℂ) (t : Circle) : ℝ

The pointwise circle modulus defect relative to a background function F₀.

Equations

• HermiteLEAN.circleModulusDefect F0 G t = |‖F0 t + G t‖ - ‖F0 t‖|

noncomputable def HermiteLEAN.circleDefectNormSq (F0 G : Circle → ℂ) : ℝ

The circle squared defect norm relative to a background function F₀.

Equations

• HermiteLEAN.circleDefectNormSq F0 G = ∫ (t : AddCircle HermiteLEAN.T), HermiteLEAN.circleModulusDefect F0 G t ^ 2 ∂AddCircle.haarAddCircle

def HermiteLEAN.annulus (j : ℕ) : Set ℂ

The annulus A_j = { z : j ≤ |z| < j + 1 }.

Equations

• HermiteLEAN.annulus j = {z : ℂ | ↑j ≤ ‖z‖ ∧ ‖z‖ < ↑(j + 1)}

noncomputable def HermiteLEAN.annulusIntegralSq (F : ℂ → ℂ) (j : ℕ) : ℝ

The weighted squared mass of a function on annulus A_j.

Equations

• HermiteLEAN.annulusIntegralSq F j = 1 / Real.pi * ∫ (z : ℂ) in HermiteLEAN.annulus j, ‖F z‖ ^ 2 * Real.exp (-‖z‖ ^ 2)

def HermiteLEAN.squareBlock (ℓ : ℕ) : Finset ℕ

The square block I_ℓ = { n : ℓ² ≤ n < (ℓ + 1)² }.

Equations

• HermiteLEAN.squareBlock ℓ = Finset.Ico (ℓ ^ 2) ((ℓ + 1) ^ 2)

def HermiteLEAN.blockIndex (n : ℕ) : ℕ

The block index of a positive Hermite mode.

Equations

• HermiteLEAN.blockIndex n = n.sqrt

noncomputable def HermiteLEAN.blockPiece {D : ℕ} (a : Fin D → ℂ) (ℓ : ℕ) : ℂ → ℂ

The ℓ-th block of a finite Hermite perturbation.

Equations

• HermiteLEAN.blockPiece a ℓ z = ∑ n : Fin D, if HermiteLEAN.blockIndex (↑n + 1) = ℓ then a n * HermiteLEAN.phi (↑n + 1) z else 0

noncomputable def HermiteLEAN.localPiece {D : ℕ} (a : Fin D → ℂ) (M j : ℕ) : ℂ → ℂ

The local part V_j built from blocks at distance at most M from j.

Equations

• HermiteLEAN.localPiece a M j z = ∑ n : Fin D, if (HermiteLEAN.blockIndex (↑n + 1)).dist j ≤ M then a n * HermiteLEAN.phi (↑n + 1) z else 0

noncomputable def HermiteLEAN.remainderPiece {D : ℕ} (a : Fin D → ℂ) (M j : ℕ) : ℂ → ℂ

The distant remainder R_j = G - V_j.

Equations

• HermiteLEAN.remainderPiece a M j z = HermiteLEAN.hermiteSum a z - HermiteLEAN.localPiece a M j z

noncomputable def HermiteLEAN.blockCoeffNormSq {D : ℕ} (a : Fin D → ℂ) (ℓ : ℕ) : ℝ

The coefficient-side squared norm of one block.

Equations

• HermiteLEAN.blockCoeffNormSq a ℓ = ∑ n : Fin D, if HermiteLEAN.blockIndex (↑n + 1) = ℓ then ‖a n‖ ^ 2 else 0

noncomputable def HermiteLEAN.h1Series (a : ℕ → ℂ) (z : ℂ) : ℂ

The formal Hermite expansion associated to a coefficient sequence.

Equations

• HermiteLEAN.h1Series a z = ∑' (n : ℕ), a n * HermiteLEAN.phi n z

def HermiteLEAN.H1 : Set (ℂ → ℂ)

The model space H₁, encoded as the closed span of the Hermite family.

Equations

• HermiteLEAN.H1 = ↑(Submodule.span ℂ (Set.range HermiteLEAN.phi)).topologicalClosure

def HermiteLEAN.H1Orthogonal : Set (ℂ → ℂ)

The closed span of the higher Hermite modes Φ₁, Φ₂, ....

Equations

• HermiteLEAN.H1Orthogonal = ↑(Submodule.span ℂ (Set.range fun (n : ℕ) => HermiteLEAN.phi (n + 1))).topologicalClosure

noncomputable def HermiteLEAN.gaussianTail (c : ℝ) (M : ℕ) : ℝ

The Gaussian tail appearing in the leakage coefficient.

Equations

• HermiteLEAN.gaussianTail c M = ∑' (m : ℕ), Real.exp (-c * HermiteLEAN.posPart (↑(m + M + 1) - 4) ^ 2)

noncomputable def HermiteLEAN.etaCoeff (Cblk cblk : ℝ) (M : ℕ) : ℝ

The leakage coefficient η_M.

Equations

• HermiteLEAN.etaCoeff Cblk cblk M = 2 * Cblk * HermiteLEAN.gaussianTail cblk M