Constructing the measurable resolvent good event

The quantitative operator event used in paper §3.4 is not presented as a measurable set: its defining operator-valued random variables are only specified almost everywhere. This file replaces its bad set by a measurable envelope of the same measure. The envelope also absorbs the two null sets on which the physical coefficient realization and the measurable Fredholm realization may disagree with their samplewise versions.

This closes the set-theoretic and measurability gap between the paper-scale L² good-event estimate and FixedModeGoodEventData.

theorem Anderson4D.MainGoodEvent.fullParametrixReal_eq_truncatedParametrixFiniteModeReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) (hA : A = truncOrder ε) : fullParametrixReal M ρ lam ε s modes c ω = truncatedParametrixFiniteModeReal M ρ lam ε A s modes c ω

The samplewise moving truncation and the finite physical-parametrix coefficient use exactly the same normalization.

def Anderson4D.MainGoodEvent.coefficientFailure (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (A s : ℕ) (modes : Fin s → Z4 × Z4) : Set M.Ω

Failure of the physical-operator coefficient realization for one finite family of modes.

Equations

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

def Anderson4D.MainGoodEvent.fredholmFailure (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Set M.Ω

Failure of the almost-sure identification between the Borel Fredholm coefficient and its samplewise inverse realization.

Equations

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

def Anderson4D.MainGoodEvent.bad (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Set M.Ω

The full bad set: the paper's quantitative operator failure together with the two representation-null sets.

Equations

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

def Anderson4D.MainGoodEvent.good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Set M.Ω

A measurable subset of the raw good event obtained by taking a measurable envelope of the full bad set.

Equations

• Anderson4D.MainGoodEvent.good M ρ lam ε s modes c = (MeasureTheory.toMeasurable MeasureTheory.volume (Anderson4D.MainGoodEvent.bad M ρ lam ε s modes c))ᶜ

theorem Anderson4D.MainGoodEvent.measurableSet_good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : MeasurableSet (good M ρ lam ε s modes c)

theorem Anderson4D.MainGoodEvent.good_subset_raw (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : good M ρ lam ε s modes c ⊆ PartialPairing.canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (PartialPairing.canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (PartialPairing.canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε))

theorem Anderson4D.MainGoodEvent.good_avoids_coefficientFailure (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) {ω : M.Ω} (hω : ω ∈ good M ρ lam ε s modes c) : ω ∉ coefficientFailure M ρ lam ε (truncOrder ε) s modes

theorem Anderson4D.MainGoodEvent.good_avoids_fredholmFailure (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) {ω : M.Ω} (hω : ω ∈ good M ρ lam ε s modes c) : ω ∉ fredholmFailure M ρ lam ε s modes c

theorem Anderson4D.MainGoodEvent.measureReal_compl_good_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) {δ : ℝ} (hraw : MeasureTheory.volume.real (PartialPairing.canonicalOneSidedL2ParametrixGoodEvent M ρ lam ε (truncOrder ε) (PartialPairing.canonicalGradedTruncatedParametrixL2Factor M ρ lam ε (truncOrder ε)) (PartialPairing.canonicalPerrLeftRemainder M ρ lam ε (truncOrder ε)))ᶜ ≤ δ) (hcoeff : ∀ᵐ (ω : M.Ω), ∀ (j : Fin s), torusFourierMatrixCoeff (canonicalPositiveTruncatedParametrixL2Operator M ρ lam ε (truncOrder ε) ω) (modes j).1 (modes j).2 = (↑paperTorusVolume)⁻¹ * ∑ n ∈ Finset.range (truncOrder ε), pmCoeff M ρ lam ε (n + 1) (modes j).1 (modes j).2 ω) (hfred : ∀ᵐ (ω : M.Ω), measurableFredholmFiniteModeReal M ρ lam ε s modes c ω = fredholmFiniteModeReal M ρ lam ε s modes c ω) : MeasureTheory.volume.real (good M ρ lam ε s modes c)ᶜ ≤ δ

Adding the two almost-sure representation failures does not enlarge the paper's exceptional-set bound.

theorem Anderson4D.MainGoodEvent.norm_fullParametrixReal_sub_fullResolventReal_le_on_good (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) (hεpos : 0 < ε) (hεsmall : 2 * ε ^ 2 ≤ 1) (hεpow : ε ^ 28 < 1 / 2) (hω : ω ∈ good M ρ lam ε s modes c) : ‖fullParametrixReal M ρ lam ε s modes c ω - fullResolventReal M ρ lam ε s modes c ω‖ ≤ ∑ j : Fin s, ‖c j‖ * (‖↑paperTorusVolume * (↑(lamEps lam ε))⁻¹‖ * ε ^ 12)

On the measurable trimmed event, the moving coefficient truncation is close to the Borel Fredholm realization by the same paper-scale error.

noncomputable def Anderson4D.MainGoodEvent.error {s : ℕ} (c : Fin s → ℂ) (lam ε : ℝ) : ℝ

The finite Cramér--Wold error supplied by the one-sided Fredholm comparison.

Equations

• Anderson4D.MainGoodEvent.error c lam ε = ∑ j : Fin s, ‖c j‖ * Anderson4D.fredholmModeErrorScale lam ε

theorem Anderson4D.MainGoodEvent.error_nonneg {s : ℕ} (c : Fin s → ℂ) (lam ε : ℝ) : 0 ≤ error c lam ε

theorem Anderson4D.MainGoodEvent.tendsto_error {s : ℕ} (c : Fin s → ℂ) {lam : ℝ} (hlam : 0 < lam) : Filter.Tendsto (error c lam) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem Anderson4D.MainGoodEvent.nonempty_fixedModeGoodEventData_of_deterministic_bounds {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant Crenorm lam : ℝ} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hCrenorm : 0 ≤ Crenorm) (hlam : 0 < lam) (hlamle : lam ≤ 1) (hpowerRatio : powerConstant * lam ≤ PartialPairing.boundaryGeometricRatio) (hrenormRatio : Crenorm * lam ≤ PartialPairing.boundaryGeometricRatio) (hdet : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (hcounter : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ q ∈ Finset.Icc 1 (truncOrder ε), |renormC2q ρ lam ε q| ≤ ε⁻¹ ^ 2 / |Real.log ε| * (Crenorm * lam) ^ (2 * q)) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Nonempty (FixedModeGoodEventData M ρ lam s modes c)

The deterministic P-3.5b and R-322 bounds construct the exact measurable good-event package consumed by the final characteristic-function replacement. No measurability premise on the raw operator event is needed.