Canonical L² operators from parametrix Fourier coefficients

An ℓ² matrix does not give an absolutely summable series of rank-one operators. This file instead proves a finite Hilbert--Schmidt bound and uses the unconditional Cauchy criterion to sum the rank-one series in operator norm. The resulting bounded operator has exactly the prescribed Fourier matrix coefficients.

The second half applies this construction to each random parametrix order. P-3.5b and the lattice summation prove simultaneous square summability almost surely, which is the correct probabilistic quantifier for the canonical realization.

noncomputable def Anderson4D.torusFourierRankOne (p : Z4 × Z4) : ↥TorusL2 →L[ℂ] ↥TorusL2

Equations

• Anderson4D.torusFourierRankOne p = ((InnerProductSpace.rankOne ℂ) (Anderson4D.torusFourierBasis (-p.1))) (Anderson4D.torusFourierBasis p.2)

theorem Anderson4D.torusFourierMatrixCoeff_rankOne (p : Z4 × Z4) (α β : Z4) : torusFourierMatrixCoeff (torusFourierRankOne p) α β = if p = (α, β) then 1 else 0

noncomputable def Anderson4D.finiteFourierMatrixOperator (a : Z4 × Z4 → ℂ) (s : Finset (Z4 × Z4)) : ↥TorusL2 →L[ℂ] ↥TorusL2

Equations

• Anderson4D.finiteFourierMatrixOperator a s = ∑ p ∈ s, a p • Anderson4D.torusFourierRankOne p

theorem Anderson4D.torusFourierMatrixCoeff_finiteFourierMatrixOperator (a : Z4 × Z4 → ℂ) (s : Finset (Z4 × Z4)) (α β : Z4) : torusFourierMatrixCoeff (finiteFourierMatrixOperator a s) α β = if (α, β) ∈ s then a (α, β) else 0

theorem Anderson4D.operatorNormSq_le_tsum_prod_fourierMatrixCoeff (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (hsum : Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff A p.1 p.2‖ ^ 2) : ‖A‖ ^ 2 ≤ ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff A p.1 p.2‖ ^ 2

theorem Anderson4D.normSq_finiteFourierMatrixOperator_le (a : Z4 × Z4 → ℂ) (s : Finset (Z4 × Z4)) : ‖finiteFourierMatrixOperator a s‖ ^ 2 ≤ ∑ p ∈ s, ‖a p‖ ^ 2

theorem Anderson4D.summable_fourierMatrixSeries (a : Z4 × Z4 → ℂ) (hsq : Summable fun (p : Z4 × Z4) => ‖a p‖ ^ 2) : Summable fun (p : Z4 × Z4) => a p • torusFourierRankOne p

noncomputable def Anderson4D.torusFourierMatrixCoeffCLM (α β : Z4) : (↥TorusL2 →L[ℂ] ↥TorusL2) →L[ℂ] ℂ

The continuous functional extracting one signed Fourier matrix coefficient from a bounded operator.

Equations

• Anderson4D.torusFourierMatrixCoeffCLM α β = (innerSL ℂ) (Anderson4D.torusFourierBasis (-α)) ∘SL (ContinuousLinearMap.apply ℂ ↥Anderson4D.TorusL2) (Anderson4D.torusFourierBasis β)

@[simp]

theorem Anderson4D.torusFourierMatrixCoeffCLM_apply (α β : Z4) (A : ↥TorusL2 →L[ℂ] ↥TorusL2) : (torusFourierMatrixCoeffCLM α β) A = torusFourierMatrixCoeff A α β

noncomputable def Anderson4D.squareSummableFourierOperator (a : Z4 × Z4 → ℂ) : ↥TorusL2 →L[ℂ] ↥TorusL2

The canonical bounded operator associated with an ℓ² Fourier matrix. Square summability is used in the theorems below to prove that the unconditional tsum has the intended value.

Equations

• Anderson4D.squareSummableFourierOperator a = ∑' (p : Anderson4D.Z4 × Anderson4D.Z4), a p • Anderson4D.torusFourierRankOne p

theorem Anderson4D.torusFourierMatrixCoeff_smul_rankOne (a : Z4 × Z4 → ℂ) (p : Z4 × Z4) (α β : Z4) : torusFourierMatrixCoeff (a p • torusFourierRankOne p) α β = if p = (α, β) then a (α, β) else 0

theorem Anderson4D.torusFourierMatrixCoeff_squareSummableFourierOperator (a : Z4 × Z4 → ℂ) (hsq : Summable fun (p : Z4 × Z4) => ‖a p‖ ^ 2) (α β : Z4) : torusFourierMatrixCoeff (squareSummableFourierOperator a) α β = a (α, β)

Canonical random parametrix operators

noncomputable def Anderson4D.parametrixOrderFourierMatrix (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (ω : M.Ω) (p : Z4 × Z4) : ℂ

The probability-Haar Fourier matrix associated with the paper's order-m coefficient.

Equations

• Anderson4D.parametrixOrderFourierMatrix M ρ lam ε m ω p = (↑Anderson4D.paperTorusVolume)⁻¹ * Anderson4D.pmCoeff M ρ lam ε m p.1 p.2 ω

theorem Anderson4D.parametrixOrderFourierMatrix_weighted_measurable_and_bound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (hε : 0 < ε) (hεle : ε ≤ 1) : AEMeasurable (fun (ω : M.Ω) => ENNReal.ofReal (‖parametrixOrderFourierMatrix M ρ lam ε m ω (α, β)‖ ^ 2 * paperL2FourierWeight ε α β)) MeasureTheory.volume ∧ ∫⁻ (ω : M.Ω), ENNReal.ofReal (‖parametrixOrderFourierMatrix M ρ lam ε m ω (α, β)‖ ^ 2 * paperL2FourierWeight ε α β) ≤ ENNReal.ofReal (parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m α β)

The raw, scaled P-3.5b coefficient has the measurable weighted second-moment bound used in the Tonelli argument. This is the operator-free version of parametrixOrder_weightedCoeff_measurable_and_bound.

theorem Anderson4D.ae_summable_parametrixOrderFourierMatrix {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (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) => ‖parametrixOrderFourierMatrix M ρ lam ε m ω p‖ ^ 2

P-3.5b plus the explicit lattice majorant make the whole order-m Fourier matrix square summable simultaneously, outside one null set.

noncomputable def Anderson4D.canonicalParametrixOrderL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

The canonical bounded operator for one random parametrix order. The unconditional tsum is totalized by mathlib, while the preceding theorem proves that it is the intended sum almost surely.

Equations

• Anderson4D.canonicalParametrixOrderL2Operator M ρ lam ε m ω = Anderson4D.squareSummableFourierOperator (Anderson4D.parametrixOrderFourierMatrix M ρ lam ε m ω)

theorem Anderson4D.canonicalParametrixOrderL2Operator_realizes {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (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) : ParametrixOrderL2CoeffRealization M ρ lam ε m (canonicalParametrixOrderL2Operator M ρ lam ε m)

The canonical order operator realizes all Fourier coefficients simultaneously almost surely.

theorem Anderson4D.nonempty_parametrixOrderL2CoeffRealization {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (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) : Nonempty { A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2 // ParametrixOrderL2CoeffRealization M ρ lam ε m A }

P-3.5b constructs, rather than assumes, an orderwise bounded operator realization.

theorem Anderson4D.lintegral_canonicalParametrixOrder_normSq_le_explicit {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (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 (‖canonicalParametrixOrderL2Operator M ρ lam ε m ω‖ ^ 2) ≤ ENNReal.ofReal (32768 * parametrixOrderL2Scalar outerConstant powerConstant lam ε m * ε⁻¹ ^ 20 * (∑' (k : Z4), l2LatticeRadialWeight 5 k) ^ 2)

The closed orderwise P-L² estimate with no externally supplied operator realization.

noncomputable def Anderson4D.canonicalPositiveTruncatedParametrixL2Operator (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

The positive-order part of the finite parametrix operator, ∑_{m=1}^A P_m, on L².

Order zero is deliberately excluded: P₀ = G is bounded but is not Hilbert--Schmidt in dimension four, so its Fourier matrix is not in ℓ² (Z4 × Z4) and cannot pass through squareSummableFourierOperator. The full physical truncation adds greenL2Op separately in L2Quantitative.lean.

Equations

• Anderson4D.canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω = ∑ n ∈ Finset.range A, Anderson4D.canonicalParametrixOrderL2Operator M ρ lam ε (n + 1) ω

theorem Anderson4D.torusFourierMatrixCoeff_finsetSum {ι : Type u_1} (s : Finset ι) (F : ι → ↥TorusL2 →L[ℂ] ↥TorusL2) (α β : Z4) : torusFourierMatrixCoeff (∑ i ∈ s, F i) α β = ∑ i ∈ s, torusFourierMatrixCoeff (F i) α β

Fourier coefficients commute with a finite operator sum.

theorem Anderson4D.canonicalPositiveTruncatedParametrixL2Operator_coeff {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {A : ℕ} (hreal : ∀ n ∈ Finset.range A, ParametrixOrderL2CoeffRealization M ρ lam ε (n + 1) (canonicalParametrixOrderL2Operator M ρ lam ε (n + 1))) : ∀ᵐ (ω : M.Ω), ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω) α β = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range A, pmCoeff M ρ lam ε (n + 1) α β ω

If every positive canonical order has its P-3.5b realization, the finite positive-order operator realizes the corresponding paper coefficients on one common full-measure event.

theorem Anderson4D.canonicalPositiveTruncatedParametrixL2Operator_coeff_of_momentBounds {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ A → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ A → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) : ∀ᵐ (ω : M.Ω), ∀ (α β : Z4), torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε A ω) α β = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range A, pmCoeff M ρ lam ε (n + 1) α β ω

Concrete construction of the positive-order coefficient identity from P-3.5b data.