Good-event replacement at the characteristic-function level

Paper §3.4 Step 2 only needs to replace the parametrix by the true resolvent in finitely many scalar Fourier tests. This file proves that replacement directly for characteristic functions, avoiding any unnecessary tightness or Prokhorov argument.

theorem Anderson4D.norm_exp_I_mul_ofReal (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ = 1

The complex unit-circle exponential has norm one.

theorem Anderson4D.norm_integral_exp_I_sub_le_error_add_bad {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X Y : Ω → ℝ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (good : Set Ω) (hgood : MeasurableSet good) (error : ℝ) (herror : 0 ≤ error) (hclose : ∀ ω ∈ good, ‖X ω - Y ω‖ ≤ error) : ‖∫ (ω : Ω), Complex.exp (Complex.I * ↑(X ω)) ∂μ - ∫ (ω : Ω), Complex.exp (Complex.I * ↑(Y ω)) ∂μ‖ ≤ error + 2 * μ.real goodᶜ

Quantitative fixed-mode replacement estimate.

On good, the two real phases differ by at most error; on its complement the two unit-circle values differ by at most two.

theorem Anderson4D.tendsto_integral_exp_I_of_goodEvent_replace {ι : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {l : Filter ι} {z : ℂ} (X Y : ι → Ω → ℝ) (hXlim : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), Complex.exp (Complex.I * ↑(X i ω)) ∂μ) l (nhds z)) (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hY : ∀ (i : ι), AEMeasurable (Y i) μ) (good : ι → Set Ω) (hgood : ∀ (i : ι), MeasurableSet (good i)) (error : ι → ℝ) (herror_nonneg : ∀ᶠ (i : ι) in l, 0 ≤ error i) (herror : Filter.Tendsto error l (nhds 0)) (hbad : Filter.Tendsto (fun (i : ι) => μ.real (good i)ᶜ) l (nhds 0)) (hclose : ∀ᶠ (i : ι) in l, ∀ ω ∈ good i, ‖X i ω - Y i ω‖ ≤ error i) : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), Complex.exp (Complex.I * ↑(Y i ω)) ∂μ) l (nhds z)

Characteristic-function convergence is unchanged by a uniformly small error on measurable events whose complements vanish in probability.

noncomputable def Anderson4D.fullResolventReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ℝ

The real scalar formed from a fixed finite family of true resolvent Fourier coefficients.

Equations

• Anderson4D.fullResolventReal M ρ lam ε s modes c ω = Anderson4D.measurableFredholmFiniteModeReal M ρ lam ε s modes c ω

theorem Anderson4D.measurable_fullResolventReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Measurable (fullResolventReal M ρ lam ε s modes c)

A finite real Fourier test of the true Fredholm resolvent is measurable. The underlying measurable potential realization agrees almost surely with the samplewise mollified potential for ε > 0.

theorem Anderson4D.Prop36.tendsto_fullResolventChar_of_second_moment_and_goodEvent {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (hsmall : hP36.boundConstant * lam < 1) (hsub : lam ^ 2 < 2 * Real.pi ^ 2) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (K q : ℝ) (hK : 0 ≤ K) (hq0 : 0 ≤ q) (hq1 : q < 1) (hsecond : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (j : Fin s) (n : ℕ), 1 ≤ n → n ≤ truncOrder ε → MeasureTheory.MemLp (pmCoeff M ρ lam ε n (modes j).1 (modes j).2) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε n (modes j).1 (modes j).2 ω‖ ^ 2 ≤ (‖↑(lamEps lam ε)‖ * K * q ^ (n - 1)) ^ 2) (good : ℝ → Set M.Ω) (hgood : ∀ (ε : ℝ), MeasurableSet (good ε)) (error : ℝ → ℝ) (herror_nonneg : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 ≤ error ε) (herror : Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (hbad : Filter.Tendsto (fun (ε : ℝ) => MeasureTheory.volume.real (good ε)ᶜ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (hclose : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ ω ∈ good ε, ‖fullParametrixReal M ρ lam ε s modes c ω - fullResolventReal M ρ lam ε s modes c ω‖ ≤ error ε) : Filter.Tendsto (fun (ε : ℝ) => ∫ (ω : M.Ω), Complex.exp (Complex.I * ↑(fullResolventReal M ρ lam ε s modes c ω))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))

Complete assembly interface: (3.24) controls the moving parametrix, while the Step 2 good event transfers its characteristic function to the true resolvent modes.

theorem Anderson4D.tendsto_fullResolventChar_on_Ioo_of_Ioi {M : NoiseModel} (ρ : SmoothCutoff) (lam : ℝ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (h : Filter.Tendsto (fun (ε : ℝ) => ∫ (ω : M.Ω), Complex.exp (Complex.I * ↑(fullResolventReal M ρ lam ε s modes c ω))) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))) : Filter.Tendsto (fun (ε : ℝ) => ∫ (ω : M.Ω), Complex.exp (Complex.I * ↑(fullResolventReal M ρ lam ε s modes c ω))) (nhdsWithin 0 (Set.Ioo 0 1)) (nhds ↑(Real.exp (-limitVar lam modes c / 2)))

Restrict the positive-side characteristic-function limit to the paper's (0,1) parameter range and present the real Gaussian characteristic function in the exact form used by MainStatement.