Two-scale characteristic-function glue

This file isolates the analytic glue in paper (3.39). The probabilistic input is a uniform-in-ε approximation of the full scalar characteristic function by its fixed perturbative truncations. The fixed-truncation moment method and the B → ∞ covariance computation then identify the limit.

theorem Anderson4D.norm_exp_I_mul_sub_exp_I_mul_le (x y : ℝ) : ‖Complex.exp (Complex.I * ↑x) - Complex.exp (Complex.I * ↑y)‖ ≤ ‖x - y‖

The unit-circle exponential is one-Lipschitz in its real phase.

theorem Anderson4D.norm_integral_exp_I_sub_le_integral_norm_sub {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X Y : Ω → ℝ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hXY : MeasureTheory.Integrable (fun (ω : Ω) => ‖X ω - Y ω‖) μ) : ‖∫ (ω : Ω), Complex.exp (Complex.I * ↑(X ω)) ∂μ - ∫ (ω : Ω), Complex.exp (Complex.I * ↑(Y ω)) ∂μ‖ ≤ ∫ (ω : Ω), ‖X ω - Y ω‖ ∂μ

Difference of characteristic-function integrals is bounded by the L¹ distance of the two real random variables.

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

The scalar test of the full moving parametrix cutoff A = ⌊|log ε|⌋.

Equations

• Anderson4D.fullParametrixReal M ρ lam ε s modes c ω = Anderson4D.fixedTruncationReal M ρ lam ε (Anderson4D.truncOrder ε) s modes c ω

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

Characteristic-function integral of the moving parametrix cutoff.

Equations

• Anderson4D.fullParametrixChar M ρ lam ε s modes c = ∫ (ω : M.Ω), Complex.exp (Complex.I * ↑(Anderson4D.fullParametrixReal M ρ lam ε s modes c ω))

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

Orders strictly above B and at most A, with the same normalization as fixedTruncationModeSum.

Equations

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

theorem Anderson4D.fixedTruncationModeSum_sub_eq_parametrixModeTail (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {B A s : ℕ} (hBA : B ≤ A) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : fixedTruncationModeSum M ρ lam ε A s modes c ω - fixedTruncationModeSum M ρ lam ε B s modes c ω = parametrixModeTail M ρ lam ε B A s modes c ω

Exact finite-sum subtraction underlying the truncation tail.

theorem Anderson4D.fullParametrixReal_sub_fixedTruncationReal (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {B s : ℕ} (hB : B ≤ truncOrder ε) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : fullParametrixReal M ρ lam ε s modes c ω - fixedTruncationReal M ρ lam ε B s modes c ω = (parametrixModeTail M ρ lam ε B (truncOrder ε) s modes c ω).re

Real-part version of the exact moving-cutoff tail identity.

theorem Anderson4D.norm_parametrixModeTail_re_le (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (B A s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ‖(parametrixModeTail M ρ lam ε B A s modes c ω).re‖ ≤ ‖(↑(lamEps lam ε))⁻¹‖ * ∑ j : Fin s, ‖c j‖ * ∑ m ∈ Finset.Ico B A, ‖pmCoeff M ρ lam ε (m + 1) (modes j).1 (modes j).2 ω‖

Pointwise triangle bound for the perturbative tail.

theorem Anderson4D.Prop36.measurable_pmCoeff {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) {m : ℕ} (hm : 1 ≤ m) (α β : Z4) (ε : ℝ) : Measurable (pmCoeff M ρ lam ε m α β)

Proposition 3.6 records measurability of every positive-order mode coefficient.

theorem Anderson4D.Prop36.integrable_pmCoeff {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) {m : ℕ} (hm : 1 ≤ m) (α β : Z4) (ε : ℝ) : MeasureTheory.Integrable (pmCoeff M ρ lam ε m α β) MeasureTheory.volume

Proposition 3.6 records integrability of every positive-order mode coefficient (the family-size-one specialization).

theorem Anderson4D.Prop36.integral_norm_parametrixModeTail_re_le {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (ε : ℝ) (B A s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ∫ (ω : M.Ω), ‖(parametrixModeTail M ρ lam ε B A s modes c ω).re‖ ≤ ‖(↑(lamEps lam ε))⁻¹‖ * ∑ j : Fin s, ‖c j‖ * ∑ m ∈ Finset.Ico B A, ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε (m + 1) (modes j).1 (modes j).2 ω‖

Integrating the pointwise tail bound commutes the two finite sums with expectation.

theorem Anderson4D.Prop36.charFun_fixedTruncationLaw_one_eq_integral {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : MeasureTheory.charFun (fixedTruncationLaw M ρ lam ε B s modes c) 1 = ∫ (ω : M.Ω), Complex.exp (Complex.I * ↑(fixedTruncationReal M ρ lam ε B s modes c ω))

Rewrite the fixed-truncation pushforward characteristic function as an expectation on the original noise space.

theorem Anderson4D.Prop36.norm_fullParametrixChar_sub_fixed_le {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (ε : ℝ) {B s : ℕ} (hB : B ≤ truncOrder ε) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ‖fullParametrixChar M ρ lam ε s modes c - MeasureTheory.charFun (fixedTruncationLaw M ρ lam ε B s modes c) 1‖ ≤ ‖(↑(lamEps lam ε))⁻¹‖ * ∑ j : Fin s, ‖c j‖ * ∑ m ∈ Finset.Ico B (truncOrder ε), ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε (m + 1) (modes j).1 (modes j).2 ω‖

The characteristic-function truncation error is controlled by the sum of the expected absolute values of the omitted mode coefficients.

theorem Anderson4D.Prop36.tendsto_charFun_of_fixedTruncation_approximation {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 → ℂ) (fullChar : ℝ → ℂ) (error : ℕ → ℝ) (herror : Filter.Tendsto error Filter.atTop (nhds 0)) (hclose : ∀ (B : ℕ), ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), dist (fullChar ε) (MeasureTheory.charFun (fixedTruncationLaw M ρ lam ε B s modes c) 1) ≤ error B) : Filter.Tendsto fullChar (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(↑(limitVar lam modes c) / 2))))

Abstract form of the final ε → 0, then B → ∞ argument.

The only missing input at this boundary is the uniform characteristic- function tail estimate supplied by (3.24).