The lattice summation behind the L² parametrix bound

This file proves the deterministic summation step (3.31) following the weighted Fourier operator estimate (3.30). The endpoint factors are convolved after the shear

(α, β) ↦ (γ, α) = (α + β, α),

and the remaining central frequency sum costs exactly ε⁻⁴ in four dimensions. Combined with the ε⁻⁸ in (3.24) and the ε⁻⁸ weight in (3.30), this preserves the paper's ε⁻²⁰ power.

noncomputable def Anderson4D.l2LatticeCoordWeight (m : ℤ) : ℝ

Equations

• Anderson4D.l2LatticeCoordWeight m = (↑m.natAbs + 1) ^ (-(5 / 4))

theorem Anderson4D.summable_l2LatticeCoordWeight : Summable l2LatticeCoordWeight

noncomputable def Anderson4D.l2LatticeProductWeight (k : Z4) : ℝ

Equations

• Anderson4D.l2LatticeProductWeight k = ∏ i : Fin Anderson4D.dim, Anderson4D.l2LatticeCoordWeight (k i)

theorem Anderson4D.summable_l2LatticeProductWeight : Summable l2LatticeProductWeight

noncomputable def Anderson4D.l2LatticeRadialWeightRpow (k : Z4) : ℝ

Equations

• Anderson4D.l2LatticeRadialWeightRpow k = (1 + Anderson4D.z4FrequencyNorm k) ^ (-5)

theorem Anderson4D.l2LatticeRadialWeightRpow_le_product (k : Z4) : l2LatticeRadialWeightRpow k ≤ l2LatticeProductWeight k

theorem Anderson4D.summable_l2LatticeRadialWeightRpow : Summable l2LatticeRadialWeightRpow

noncomputable def Anderson4D.l2LatticeRadialWeight (n : ℕ) (k : Z4) : ℝ

Equations

• Anderson4D.l2LatticeRadialWeight n k = ((1 + Anderson4D.z4FrequencyNorm k) ^ n)⁻¹

theorem Anderson4D.l2LatticeRadialWeightRpow_eq_five (k : Z4) : l2LatticeRadialWeightRpow k = l2LatticeRadialWeight 5 k

theorem Anderson4D.summable_l2LatticeRadialWeight_five : Summable (l2LatticeRadialWeight 5)

theorem Anderson4D.l2Lattice_scalar_convolution_bound {A B G : ℝ} (hA : 0 < A) (hB : 0 < B) (hG : 0 < G) (hGA : G ≤ 2 * A) : (A ^ 4)⁻¹ * (B ^ 4)⁻¹ ≤ 8 * (G ^ 3)⁻¹ * ((A ^ 5)⁻¹ + (B ^ 5)⁻¹)

theorem Anderson4D.l2Lattice_bracket_triangle (α γ : Z4) : 1 + z4FrequencyNorm γ ≤ 1 + z4FrequencyNorm α + (1 + z4FrequencyNorm (γ - α))

theorem Anderson4D.l2Lattice_convolution_term_bound (α γ : Z4) : l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α) ≤ 8 * l2LatticeRadialWeight 3 γ * (l2LatticeRadialWeight 5 α + l2LatticeRadialWeight 5 (γ - α))

theorem Anderson4D.summable_l2Lattice_convolution (γ : Z4) : Summable fun (α : Z4) => l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α)

theorem Anderson4D.tsum_l2Lattice_convolution_bound (γ : Z4) : ∑' (α : Z4), l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α) ≤ 16 * l2LatticeRadialWeight 3 γ * ∑' (α : Z4), l2LatticeRadialWeight 5 α

noncomputable def Anderson4D.l2LatticeCentralWeight (ε : ℝ) (k : Z4) : ℝ

Equations

• Anderson4D.l2LatticeCentralWeight ε k = (1 + (ε ^ 2 * Anderson4D.z4FrequencyNorm k) ^ 2)⁻¹

theorem Anderson4D.l2LatticeCentralWeight_le {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (k : Z4) : l2LatticeCentralWeight ε k ≤ 2 * ε⁻¹ ^ 4 * l2LatticeRadialWeight 2 k

theorem Anderson4D.l2LatticeRadial_three_mul_central_bound {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (k : Z4) : l2LatticeRadialWeight 3 k * l2LatticeCentralWeight ε k ≤ 2 * ε⁻¹ ^ 4 * l2LatticeRadialWeight 5 k

theorem Anderson4D.summable_l2LatticeRadial_three_mul_central {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : Summable fun (k : Z4) => l2LatticeRadialWeight 3 k * l2LatticeCentralWeight ε k

theorem Anderson4D.tsum_l2LatticeRadial_three_mul_central_bound {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : ∑' (k : Z4), l2LatticeRadialWeight 3 k * l2LatticeCentralWeight ε k ≤ 2 * ε⁻¹ ^ 4 * ∑' (k : Z4), l2LatticeRadialWeight 5 k

noncomputable def Anderson4D.l2LatticeGammaPairWeight (ε : ℝ) (p : Z4 × Z4) : ℝ

Equations

• Anderson4D.l2LatticeGammaPairWeight ε p = Anderson4D.l2LatticeCentralWeight ε p.1 * (Anderson4D.l2LatticeRadialWeight 4 p.2 * Anderson4D.l2LatticeRadialWeight 4 (p.1 - p.2))

theorem Anderson4D.l2LatticeGammaPairWeight_nonneg (ε : ℝ) (p : Z4 × Z4) : 0 ≤ l2LatticeGammaPairWeight ε p

theorem Anderson4D.summable_l2LatticeGammaPairWeight_fiber (ε : ℝ) (γ : Z4) : Summable fun (α : Z4) => l2LatticeGammaPairWeight ε (γ, α)

theorem Anderson4D.tsum_l2LatticeGammaPairWeight_fiber_bound {ε : ℝ} (γ : Z4) : ∑' (α : Z4), l2LatticeGammaPairWeight ε (γ, α) ≤ (16 * ∑' (α : Z4), l2LatticeRadialWeight 5 α) * (l2LatticeRadialWeight 3 γ * l2LatticeCentralWeight ε γ)

theorem Anderson4D.summable_l2LatticeGammaPairWeight_outer {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : Summable fun (γ : Z4) => ∑' (α : Z4), l2LatticeGammaPairWeight ε (γ, α)

theorem Anderson4D.summable_l2LatticeGammaPairWeight {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : Summable (l2LatticeGammaPairWeight ε)

theorem Anderson4D.tsum_l2LatticeGammaPairWeight_bound {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : ∑' (p : Z4 × Z4), l2LatticeGammaPairWeight ε p ≤ 32 * ε⁻¹ ^ 4 * (∑' (α : Z4), l2LatticeRadialWeight 5 α) ^ 2

def Anderson4D.l2LatticePairShear : Z4 × Z4 ≃ Z4 × Z4

Equations

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

noncomputable def Anderson4D.l2LatticePairWeight (ε : ℝ) (p : Z4 × Z4) : ℝ

Equations

• Anderson4D.l2LatticePairWeight ε p = Anderson4D.l2LatticeRadialWeight 4 p.1 * Anderson4D.l2LatticeRadialWeight 4 p.2 * Anderson4D.l2LatticeCentralWeight ε (p.1 + p.2)

theorem Anderson4D.l2LatticeGammaPairWeight_shear (ε : ℝ) (p : Z4 × Z4) : l2LatticeGammaPairWeight ε (l2LatticePairShear p) = l2LatticePairWeight ε p

theorem Anderson4D.summable_l2LatticePairWeight {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : Summable (l2LatticePairWeight ε)

theorem Anderson4D.tsum_l2LatticePairWeight_bound {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) : ∑' (p : Z4 × Z4), l2LatticePairWeight ε p ≤ 32 * ε⁻¹ ^ 4 * (∑' (α : Z4), l2LatticeRadialWeight 5 α) ^ 2

Comparison with the exact factors in (3.24) and (3.30)

theorem Anderson4D.fourthOrderModeDecay_le_l2LatticeRadialWeight (k : Z4) : fourthOrderModeDecay k ≤ 4 * l2LatticeRadialWeight 4 k

The endpoint Japanese bracket in (3.24) is controlled by the radial fourth-order weight used in the convolution estimate.

theorem Anderson4D.norm_z4EuclideanFrequency_le_two_mul_frequencyNorm (k : Z4) : ‖z4EuclideanFrequency k‖ ≤ 2 * z4FrequencyNorm k

In four dimensions the Euclidean frequency norm is at most twice the sup norm used by the deterministic ledger.

theorem Anderson4D.eighthOrderFrequencyDecay_mul_paperWeight_le_central (ε : ℝ) (k : Z4) : eighthOrderFrequencyDecay (ε ^ 2 * z4FrequencyNorm k) * (1 + (ε ^ 2 * ‖z4EuclideanFrequency k‖) ^ 2) ^ 3 ≤ 64 * l2LatticeCentralWeight ε k

The product of the eighth-order central decay in (3.24) and the sixth-order Euclidean Japanese bracket in (3.30) leaves one central second-order decay. The constant 64 is the four-dimensional Euclidean/sup-norm comparison cubed.

theorem Anderson4D.deterministicMomentDecay_mul_paperL2FourierWeight_le (ε : ℝ) (α β : Z4) : deterministicMomentDecay ε α β * paperL2FourierWeight ε α β ≤ 1024 * ε⁻¹ ^ 16 * l2LatticePairWeight ε (α, β)

Pointwise deterministic majorant for the exact product of (3.24) and the Fourier weight (3.30). The two printed ε⁻⁸ factors remain visible as ε⁻¹ ^ 16; the lattice sum below contributes the final ε⁻⁴.

noncomputable def Anderson4D.parametrixOrderL2Scalar (outerConstant powerConstant lam ε : ℝ) (m : ℕ) : ℝ

The frequency-independent factor in one order of the weighted second-moment majorant.

Equations

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

theorem Anderson4D.parametrixOrderL2Scalar_nonneg {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ parametrixOrderL2Scalar outerConstant powerConstant lam ε m

theorem Anderson4D.parametrixOrderL2WeightedMomentRHS_le_latticePair {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m α β ≤ parametrixOrderL2Scalar outerConstant powerConstant lam ε m * (1024 * ε⁻¹ ^ 16 * l2LatticePairWeight ε (α, β))

Pointwise majorization of the actual P-3.5b right side after inserting the (3.30) Fourier weight.

theorem Anderson4D.summable_parametrixOrderL2WeightedMomentRHS {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : Summable fun (p : Z4 × Z4) => parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1

The full deterministic majorant consumed by the Tonelli form of (3.30) is summable. This discharges the formerly explicit hmajorant hypothesis in the orderwise L² bridge.

theorem Anderson4D.tsum_parametrixOrderL2WeightedMomentRHS_le {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∑' (p : Z4 × Z4), parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1 ≤ 32768 * parametrixOrderL2Scalar outerConstant powerConstant lam ε m * ε⁻¹ ^ 20 * (∑' (k : Z4), l2LatticeRadialWeight 5 k) ^ 2

Numerical form of paper (3.31): the complete double Fourier sum costs ε⁻²⁰. The remaining square is a fixed finite lattice mass, independent of all paper parameters and of the order m.

Automatic almost-sure summability and the closed P-L² bound

theorem Anderson4D.ae_summable_parametrixOrder_weightedCoeff {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∀ᵐ (ω : M.Ω), Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1

Summability of the expected deterministic majorant forces the realized weighted Fourier square-sum to be finite almost surely. Thus the non-junk hsum condition used by the abstract Tonelli adapter is a consequence of P-3.5b, not an additional analytic hypothesis.

theorem Anderson4D.lintegral_parametrixOrder_normSq_le_explicit {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∫⁻ (ω : M.Ω), ENNReal.ofReal (‖A ω‖ ^ 2) ≤ ENNReal.ofReal (32768 * parametrixOrderL2Scalar outerConstant powerConstant lam ε m * ε⁻¹ ^ 20 * (∑' (k : Z4), l2LatticeRadialWeight 5 k) ^ 2)

Closed ENNReal expectation form of P-L² at one parametrix order: P-3.5b alone supplies both summability hypotheses of the abstract Tonelli adapter, and (3.31) supplies the displayed ε⁻²⁰ bound.

theorem Anderson4D.integral_parametrixOrder_normSq_le_explicit {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hintA : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖A ω‖ ^ 2) MeasureTheory.volume) : ∫ (ω : M.Ω), ‖A ω‖ ^ 2 ≤ 32768 * parametrixOrderL2Scalar outerConstant powerConstant lam ε m * ε⁻¹ ^ 20 * (∑' (k : Z4), l2LatticeRadialWeight 5 k) ^ 2

Ordinary real-integral form of the preceding explicit orderwise bound.