Finite-mode convergence in law

This file upgrades the frozen scalar characteristic-function statement to the realified finite-family convergence-in-distribution formulation of the main theorem. The random vector uses the manifestly measurable Fredholm realization. At every positive mollification scale this realization agrees almost surely with the samplewise resolvent coefficients occurring in MainStatement.

noncomputable def Anderson4D.measurableFredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (ω : M.Ω) : EuclideanSpace ℝ (Fin s × Bool)

The measurable realification of a finite family of Fredholm Fourier coefficients. false is the real coordinate and true the imaginary coordinate.

Equations

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

noncomputable def Anderson4D.fredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (ω : M.Ω) : EuclideanSpace ℝ (Fin s × Bool)

The literal samplewise Fredholm vector. This need not be manifestly measurable from its definition, but at every positive scale it is almost surely equal to measurableFredholmFiniteModeVector.

Equations

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

theorem Anderson4D.measurable_measurableFredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) : Measurable (measurableFredholmFiniteModeVector M ρ lam ε s modes)

theorem Anderson4D.ae_measurableFredholmFiniteModeVector_eq_fredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (s : ℕ) (modes : Fin s → Z4 × Z4) : measurableFredholmFiniteModeVector M ρ lam ε s modes =ᵐ[MeasureTheory.volume] fredholmFiniteModeVector M ρ lam ε s modes

The realified measurable representative agrees almost surely with the literal samplewise Fredholm mode family.

theorem Anderson4D.aemeasurable_fredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (s : ℕ) (modes : Fin s → Z4 × Z4) : AEMeasurable (fredholmFiniteModeVector M ρ lam ε s modes) MeasureTheory.volume

theorem Anderson4D.inner_measurableFredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) (ω : M.Ω) (t : EuclideanSpace ℝ (Fin s × Bool)) : inner ℝ (measurableFredholmFiniteModeVector M ρ lam ε s modes ω) t = measurableFredholmFiniteModeReal M ρ lam ε s modes (complexCoeffOfRealified t.ofLp) ω

Pairing the realified vector against a real test vector is exactly the scalar finite-mode observable with the corresponding complex coefficients.

theorem Anderson4D.ProbabilityMeasure.tendsto_of_filter_tendsto_charFun {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} [l.IsCountablyGenerated] (μ : ι → MeasureTheory.ProbabilityMeasure E) (μ₀ : MeasureTheory.ProbabilityMeasure E) (h : ∀ (t : E), Filter.Tendsto (fun (i : ι) => MeasureTheory.charFun (↑(μ i)) t) l (nhds (MeasureTheory.charFun (↑μ₀) t))) : Filter.Tendsto μ l (nhds μ₀)

Lévy's reverse implication over an arbitrary countably generated source filter, obtained by testing every sequence converging to that filter and applying mathlib's sequence-indexed Lévy theorem.

noncomputable def Anderson4D.measurableFredholmFiniteModeLaw (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (s : ℕ) (modes : Fin s → Z4 × Z4) : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin s × Bool))

The law of the measurable finite-mode Fredholm vector.

Equations

• Anderson4D.measurableFredholmFiniteModeLaw M ρ lam ε s modes = MeasureTheory.ProbabilityMeasure.map ⟨MeasureTheory.volume, ⋯⟩ ⋯

theorem Anderson4D.measurableFredholmFiniteModeLaw_eq_map_fredholmFiniteModeVector (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (s : ℕ) (modes : Fin s → Z4 × Z4) : ↑(measurableFredholmFiniteModeLaw M ρ lam ε s modes) = MeasureTheory.Measure.map (fredholmFiniteModeVector M ρ lam ε s modes) MeasureTheory.volume

At every positive scale the law used in MainLawStatement is literally the push-forward law of the samplewise Fredholm vector.

def Anderson4D.MainLawStatement (M : NoiseModel) (ρ : SmoothCutoff) : Prop

The finite-family convergence-in-distribution form of the main statement. The limit is the explicit realified Gaussian law.

Equations

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

theorem Anderson4D.mainLawStatement_of_mainStatement (M : NoiseModel) (ρ : SmoothCutoff) (hmain : MainStatement M ρ) : MainLawStatement M ρ

The scalar Cramér--Wold characteristic-function statement implies the finite-family convergence-in-distribution statement.

theorem Anderson4D.mainConditionalLaw_of_mainConditional (M : NoiseModel) (ρ : SmoothCutoff) (hmain : MainConditional M ρ) : Prop36Family M ρ → MainLawStatement M ρ

Conditional convergence in law, directly from the conditional characteristic-function theorem.