Quantitative closure of the L² parametrix step

This file completes the probability and finite-sum part of P-L2 without postulating an operator realization. The canonical operators constructed from the Fourier coefficients are strongly measurable almost everywhere. Their finite sum Q_A satisfies the elementary but indispensable estimate

E ‖Q_A‖² ≤ (A + 1) * ∑_{m=0}^A E ‖P_m‖².

The last section combines this estimate with an honest almost-everywhere P-err input. The validity of the two operator identities is included in the good event; it is not silently strengthened to a pointwise hypothesis.

Measurability of the canonical coefficient operators

theorem Anderson4D.aestronglyMeasurable_canonicalParametrixOrderL2Operator {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) : MeasureTheory.AEStronglyMeasurable (canonicalParametrixOrderL2Operator M ρ lam ε m) MeasureTheory.volume

The canonical order operator is almost everywhere strongly measurable.

The target operator space is not assumed separable. We therefore do not appeal to Borel measurability of an arbitrary operator-valued tsum. Instead, finite Fourier sums are strongly measurable and converge in operator norm almost surely by the square-summability theorem.

Explicit second-moment budgets

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

The explicit right side of the orderwise (3.31) estimate.

Equations

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

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

theorem Anderson4D.normSq_finsetSum_le_card_mul_sum_normSq {ι : Type u_1} {H : Type u_2} [NormedAddCommGroup H] (s : Finset ι) (F : ι → H) : ‖∑ i ∈ s, F i‖ ^ 2 ≤ ↑s.card * ∑ i ∈ s, ‖F i‖ ^ 2

Pointwise finite-sum estimate ‖Σ A_m‖² ≤ card(s) Σ ‖A_m‖².

theorem Anderson4D.integrable_normSq_canonicalParametrixOrderL2Operator {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) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalParametrixOrderL2Operator M ρ lam ε m ω‖ ^ 2) MeasureTheory.volume

The canonical order operator has an integrable squared norm.

theorem Anderson4D.integral_normSq_canonicalParametrixOrderL2Operator_le {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.Ω), ‖canonicalParametrixOrderL2Operator M ρ lam ε m ω‖ ^ 2 ≤ canonicalParametrixOrderL2SecondMomentBudget outerConstant powerConstant lam ε m

Real expectation form of the canonical orderwise (3.31) bound.

The physical truncation: deterministic order zero

noncomputable def Anderson4D.canonicalPhysicalParametrixL2Piece (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {A : ℕ} (i : Fin (A + 1)) : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2

One piece of the physical truncation. The zeroth piece is the bounded Green multiplier itself. Positive pieces use the canonical square-summable coefficient construction.

This distinction is forced in dimension four: G is bounded but not Hilbert--Schmidt, so its Fourier matrix must not be fed to squareSummableFourierOperator.

Equations

• Anderson4D.canonicalPhysicalParametrixL2Piece M ρ lam ε i = if ↑i = 0 then fun (x : M.Ω) => Anderson4D.greenL2Op else Anderson4D.canonicalParametrixOrderL2Operator M ρ lam ε ↑i

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

The actual finite physical parametrix P_ε = G + ∑_{m=1}^A P_m.

Equations

• Anderson4D.canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω = ∑ i : Fin (A + 1), Anderson4D.canonicalPhysicalParametrixL2Piece M ρ lam ε i ω

noncomputable def Anderson4D.canonicalPhysicalParametrixL2PieceSecondMomentBudget (outerConstant powerConstant lam ε : ℝ) {A : ℕ} (i : Fin (A + 1)) : ℝ

The orderwise budget, with the deterministic Green piece bounded by one.

Equations

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

noncomputable def Anderson4D.canonicalPhysicalTruncatedParametrixL2SecondMomentBudget (outerConstant powerConstant lam ε : ℝ) (A : ℕ) : ℝ

The finite physical budget. The factor A + 1 is exactly the cardinality in ‖Σ A_m‖² ≤ (A+1) Σ ‖A_m‖².

Equations

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

theorem Anderson4D.canonicalPhysicalParametrixL2PieceSecondMomentBudget_nonneg {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (i : Fin (A + 1)) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ canonicalPhysicalParametrixL2PieceSecondMomentBudget outerConstant powerConstant lam ε i

theorem Anderson4D.canonicalPhysicalTruncatedParametrixL2SecondMomentBudget_nonneg {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A

theorem Anderson4D.aestronglyMeasurable_canonicalPhysicalParametrixL2Piece {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (i : Fin (A + 1)) (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) : MeasureTheory.AEStronglyMeasurable (canonicalPhysicalParametrixL2Piece M ρ lam ε i) MeasureTheory.volume

theorem Anderson4D.aestronglyMeasurable_canonicalPhysicalTruncatedParametrixL2Operator {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) : MeasureTheory.AEStronglyMeasurable (canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A) MeasureTheory.volume

theorem Anderson4D.integrable_normSq_canonicalPhysicalParametrixL2Piece {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (i : Fin (A + 1)) (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) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPhysicalParametrixL2Piece M ρ lam ε i ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.integral_normSq_canonicalPhysicalParametrixL2Piece_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (i : Fin (A + 1)) (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.Ω), ‖canonicalPhysicalParametrixL2Piece M ρ lam ε i ω‖ ^ 2 ≤ canonicalPhysicalParametrixL2PieceSecondMomentBudget outerConstant powerConstant lam ε i

theorem Anderson4D.integrable_normSq_canonicalPhysicalTruncatedParametrixL2Operator {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) : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω‖ ^ 2) MeasureTheory.volume

theorem Anderson4D.integral_normSq_canonicalPhysicalTruncatedParametrixL2Operator_le {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.Ω), ‖canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω‖ ^ 2 ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A

A mixed second/first-moment good event

theorem Anderson4D.measureReal_norm_ge_le_div_secondMoment {Ω : Type u_1} {H : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (μ : MeasureTheory.Measure Ω) (F : Ω → H →L[ℂ] H) (r δ : ℝ) (hr : 0 < r) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ‖F ω‖ ^ 2) μ) (hsecond : ∫ (ω : Ω), ‖F ω‖ ^ 2 ∂μ ≤ δ) : μ.real {ω : Ω | r ≤ ‖F ω‖} ≤ δ / r ^ 2

Second-moment Markov at an arbitrary positive operator-norm threshold.

def Anderson4D.quantitativeL2ParametrixGoodEvent {Ω : Type u_1} (P Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (valid : Ω → Prop) (ε : ℝ) : Set Ω

The paper-scale event, augmented by an explicit validity predicate for the operator identities and the physical/factorized bridge.

Keeping valid inside the event permits the identities to hold only almost surely, as is natural for random kernels.

Equations

• Anderson4D.quantitativeL2ParametrixGoodEvent P Rleft Rright valid ε = {ω : Ω | ‖P ω‖ ≤ ε ^ (-14) ∧ ‖Rleft ω‖ + ‖Rright ω‖ ≤ ε ^ 28 ∧ valid ω}

theorem Anderson4D.measureReal_compl_quantitativeL2ParametrixGoodEvent_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (P Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (valid : Ω → Prop) (ε δP δR : ℝ) (hεpos : 0 < ε) (hintP : MeasureTheory.Integrable (fun (ω : Ω) => ‖P ω‖ ^ 2) μ) (hintR : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rleft ω‖ + ‖Rright ω‖) μ) (hsecondP : ∫ (ω : Ω), ‖P ω‖ ^ 2 ∂μ ≤ δP) (hfirstR : ∫ (ω : Ω), ‖Rleft ω‖ + ‖Rright ω‖ ∂μ ≤ δR) (hvalid : ∀ᵐ (ω : Ω) ∂μ, valid ω) : μ.real (quantitativeL2ParametrixGoodEvent P Rleft Rright valid ε)ᶜ ≤ δP / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

Mixed Chebyshev/Markov estimate: the parametrix uses its proved second moment, while P-err supplies the paper's first-moment remainder estimate. An almost-sure identity/bridge input costs zero measure.

The exact remaining P-err/operator bridge

def Anderson4D.canonicalFactorizedParametrixValid (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ω : M.Ω) : Prop

The almost-sure predicate still required from P-err and the physical-kernel/operator bridge. It says both that the factorized parametrix identities hold and that multiplying the factorized parametrix by G gives the canonical physical operator constructed from the coefficients.

This is a definition of the unresolved input, not an output predicate: none of its fields contains a norm estimate or a desired conclusion.

Equations

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

def Anderson4D.canonicalL2ParametrixGoodEvent (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) : Set M.Ω

The canonical paper-scale event. Its norm threshold is imposed on the physical parametrix P_ε = Qfactor * G, not on the auxiliary factorized operator.

Equations

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

theorem Anderson4D.measureReal_compl_canonicalL2ParametrixGoodEvent_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (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) (hintR : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖Rleft ω‖ + ‖Rright ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstR : ∫ (ω : M.Ω), ‖Rleft ω‖ + ‖Rright ω‖ ≤ δR) (hvalid : ∀ᵐ (ω : M.Ω), canonicalFactorizedParametrixValid M ρ lam ε A Qfactor Rleft Rright ω) : MeasureTheory.volume.real (canonicalL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft Rright)ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

Fully instantiated probability bound for the canonical finite parametrix. The only unclosed hypotheses are exactly P-3.5b/Fubini, P-wick, P-3.5b-det, and the P-err/physical-operator bridge plus its first-moment remainder estimate.

theorem Anderson4D.measureReal_compl_canonicalL2ParametrixGoodEvent_le_two_mul_sq {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (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) (hbudget : canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A ≤ ε ^ (-24)) (hintR : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖Rleft ω‖ + ‖Rright ω‖) MeasureTheory.volume) (hfirstR : ∫ (ω : M.Ω), ‖Rleft ω‖ + ‖Rright ω‖ ≤ ε ^ 30) (hvalid : ∀ᵐ (ω : M.Ω), canonicalFactorizedParametrixValid M ρ lam ε A Qfactor Rleft Rright ω) : MeasureTheory.volume.real (canonicalL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft Rright)ᶜ ≤ 2 * ε ^ 2

If the finite-sum budget and the two remainders have the powers used in paper (3.32), the exceptional set is at most 2 ε². The explicit factor two records the union bound.

Inversion using the left correction

theorem Anderson4D.inverseGreen_eq_correctedParametrixLeft_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1) (hRright : ‖Rright‖ < 1) : inverseGreen G M ⋯ = oneAddNeumannInverse Rleft hRleft * Q * G

Left-corrected version of the inverse formula. This orientation is the one whose error is controlled by the norm of the physical parametrix Q * G.

theorem Anderson4D.norm_inverseGreen_sub_parametrix_mul_le_two_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] (G M Q Rleft Rright : H →L[ℂ] H) (hdata : AndersonParametrixData G M Q Rleft Rright) (hRleft : ‖Rleft‖ < 1 / 2) (hRright : ‖Rright‖ < 1 / 2) : ‖inverseGreen G M ⋯ - Q * G‖ ≤ 2 * ‖Rleft‖ * ‖Q * G‖

Quantitative left-corrected error, depending on ‖QG‖ rather than the auxiliary factorized norm ‖Q‖.

Pointwise canonical inversion on the good event

theorem Anderson4D.lopInvertible_on_canonicalL2ParametrixGoodEvent (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hεpow : ε ^ 28 < 1 / 2) {ω : M.Ω} (hω : ω ∈ canonicalL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft Rright) : LopInvertible greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω)

theorem Anderson4D.norm_inverseGreen_sub_canonicalParametrix_on_goodEvent (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hεpos : 0 < ε) (hεsmall : 2 * ε ^ 2 ≤ 1) (hεpow : ε ^ 28 < 1 / 2) {ω : M.Ω} (hω : ω ∈ canonicalL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft Rright) : ‖inverseGreen greenL2Op (mollifiedPotentialL2Op M ρ lam ε ω) ⋯ - canonicalPhysicalTruncatedParametrixL2Operator M ρ lam ε A ω‖ ≤ ε ^ 12

Paper (3.33), now attached to the canonical coefficient operator and requiring P-err only through the validity conjunct of the event.