Geometric closure of the moving parametrix tail

This file turns the order-by-order L¹ estimate obtained from paper (3.24) into the uniform geometric truncation estimate (3.35). It is kept separate from the second-moment proof so that the latter only has to expose its natural coefficient-level interface.

theorem Anderson4D.integral_norm_le_sqrt_integral_norm_sq {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → E) (hf : MeasureTheory.MemLp f 2 μ) : ∫ (ω : Ω), ‖f ω‖ ∂μ ≤ √(∫ (ω : Ω), ‖f ω‖ ^ 2 ∂μ)

On a probability space, Cauchy--Schwarz bounds the first absolute moment by the square root of the second absolute moment.

theorem Anderson4D.integral_norm_le_of_integral_norm_sq_le_sq {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → E) (hf : MeasureTheory.MemLp f 2 μ) {R : ℝ} (hR : 0 ≤ R) (hsecond : ∫ (ω : Ω), ‖f ω‖ ^ 2 ∂μ ≤ R ^ 2) : ∫ (ω : Ω), ‖f ω‖ ∂μ ≤ R

Convenient squared-bound form of the L² → L¹ implication.

theorem Anderson4D.Prop36.norm_fullParametrixChar_sub_fixed_le_geometric {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (ε : ℝ) {B A s : ℕ} (hA : truncOrder ε = A) (hBA : B ≤ A) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (K q : ℝ) (hK : 0 ≤ K) (hq0 : 0 ≤ q) (hq1 : q < 1) (hlamEps : lamEps lam ε ≠ 0) (hcoeff : ∀ (j : Fin s), ∀ m ∈ Finset.Ico B A, ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε (m + 1) (modes j).1 (modes j).2 ω‖ ≤ ‖↑(lamEps lam ε)‖ * K * q ^ m) : ‖fullParametrixChar M ρ lam ε s modes c - MeasureTheory.charFun (fixedTruncationLaw M ρ lam ε B s modes c) 1‖ ≤ (∑ j : Fin s, ‖c j‖) * K * (q ^ B / (1 - q))

A geometric L¹ bound on the individual random coefficients gives the exact finite-tail estimate needed in (3.35).

noncomputable def Anderson4D.geometricTruncationError {s : ℕ} (c : Fin s → ℂ) (K q : ℝ) (B : ℕ) : ℝ

The geometric error appearing on the right of (3.35).

Equations

• Anderson4D.geometricTruncationError c K q B = (∑ j : Fin s, ‖c j‖) * K * (q ^ B / (1 - q))

theorem Anderson4D.tendsto_geometricTruncationError {s : ℕ} (c : Fin s → ℂ) {K q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) : Filter.Tendsto (geometricTruncationError c K q) Filter.atTop (nhds 0)

For a genuine geometric ratio, the truncation error vanishes as B → ∞.

theorem Anderson4D.Prop36.tendsto_fullParametrixChar_of_geometric_coeff_bound {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (K q : ℝ) (hK : 0 ≤ K) (hq0 : 0 ≤ q) (hq1 : q < 1) (hcoeff : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (j : Fin s) (n : ℕ), 1 ≤ n → n ≤ truncOrder ε → ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε n (modes j).1 (modes j).2 ω‖ ≤ ‖↑(lamEps lam ε)‖ * K * q ^ (n - 1)) : Filter.Tendsto (fun (ε : ℝ) => fullParametrixChar M ρ lam ε s modes c) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))

Two-scale closure of paper Step 3.

Once (3.24) has supplied a uniform geometric L¹ bound for every positive-order mode coefficient, the moving parametrix scalar converges to the Gaussian characteristic function with variance limitVar. This theorem performs the complete ε → 0, then B → ∞ argument.

theorem Anderson4D.Prop36.tendsto_fullParametrixChar_of_geometric_second_moment_bound {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (K q : ℝ) (hK : 0 ≤ K) (hq0 : 0 ≤ q) (hq1 : q < 1) (hsecond : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (j : Fin s) (n : ℕ), 1 ≤ n → n ≤ truncOrder ε → MeasureTheory.MemLp (pmCoeff M ρ lam ε n (modes j).1 (modes j).2) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε n (modes j).1 (modes j).2 ω‖ ^ 2 ≤ (‖↑(lamEps lam ε)‖ * K * q ^ (n - 1)) ^ 2) : Filter.Tendsto (fun (ε : ℝ) => fullParametrixChar M ρ lam ε s modes c) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))

Adapter from the natural squared estimate in (3.24) to the geometric L¹ interface used by the two-scale closure theorem.