Paper-faithful one-sided parametrix good event

Paper (3.32)--(3.33) controls the physical parametrix and the left factor residual

Q (1 - G M) - 1.

Compactness of G M makes this one-sided information sufficient for invertibility. This file packages the corresponding probability event and specializes it to the canonical finite parametrix and the explicit boundary sum of (3.21).

Abstract one-sided event and probability estimate

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

Mixed second/first-moment event with only the residual estimated in the paper.

Equations

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

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

The existing mixed Markov estimate, specialized with zero right residual, gives the paper-faithful one-sided exceptional-set bound.

Canonical finite factor

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

The exact one-sided identity and the physical bridge needed by the compact Fredholm argument.

Equations

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

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

The canonical paper-scale event with only the left P-err residual.

Equations

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

theorem Anderson4D.PartialPairing.canonicalOneSidedParametrixValid_of_factorized (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A : ℕ) (Qfactor Rleft Rright : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ω : M.Ω) (hvalid : canonicalFactorizedParametrixValid M ρ lam ε A Qfactor Rleft Rright ω) : canonicalOneSidedParametrixValid M ρ lam ε A Qfactor Rleft ω

Canonical probability bounds

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalOneSidedL2ParametrixGoodEvent_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {A : ℕ} (Qfactor Rleft : 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 ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstR : ∫ (ω : M.Ω), ‖Rleft ω‖ ≤ δR) (hvalid : ∀ᵐ (ω : M.Ω), canonicalOneSidedParametrixValid M ρ lam ε A Qfactor Rleft ω) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε A Qfactor Rleft)ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

theorem Anderson4D.PartialPairing.ae_canonicalOneSidedParametrixValid {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) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) : ∀ᵐ (ω : M.Ω), canonicalOneSidedParametrixValid M ρ lam ε A (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A) (canonicalPerrLeftRemainder M ρ lam ε A) ω

The canonical factor discharges the one-sided validity predicate almost surely from the already proved coefficient bridge.

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_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) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε A ω) (hintR : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPerrLeftRemainder M ρ lam ε A ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstR : ∫ (ω : M.Ω), ‖canonicalPerrLeftRemainder M ρ lam ε A ω‖ ≤ δR) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε A (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε A) (canonicalPerrLeftRemainder M ρ lam ε A))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε A / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

Exceptional-set bound with the canonical factor and only its left residual.

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_of_boundary {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hintBoundary : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖) MeasureTheory.volume) (δR : ℝ) (hfirstBoundary : ∫ (ω : M.Ω), ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖ ≤ δR) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ canonicalPhysicalTruncatedParametrixL2SecondMomentBudget outerConstant powerConstant lam ε (truncOrder ε) / (ε ^ (-14)) ^ 2 + δR / ε ^ 28

The final P-err interface is the first moment of the explicit last-block boundary sum in (3.21).

theorem Anderson4D.PartialPairing.measureReal_compl_canonicalConstructedOneSidedGoodEvent_le_two_mul_sq {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} (hfubini : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : 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 ε (truncOrder ε) ≤ ε ^ (-24)) (hagree : ∀ᵐ (ω : M.Ω), ParametrixGradedCoefficientAgreement M ρ lam ε (truncOrder ε) ω) (hintBoundary : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖) MeasureTheory.volume) (hfirstBoundary : ∫ (ω : M.Ω), ‖canonicalPerrLeftBoundary M ρ lam ε (truncOrder ε) ω‖ ≤ ε ^ 30) : MeasureTheory.volume.real (canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ 2 * ε ^ 2

Paper-scale powers give an exceptional set of size at most 2 ε²; no non-paper right residual occurs.

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

Compact Fredholm inversion on the one-sided good event.

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

Paper (3.33) from precisely the one-sided event controlled by (3.32).