Filter-indexed weak-convergence glue

Mathlib's reverse Lévy theorem is sequence-indexed, but the implication needed after a weak-convergence proof is valid over every filter: convergence in distribution gives pointwise convergence of characteristic functions. This file exposes that implication both in law form and as integrals over the original probability spaces.

theorem Anderson4D.TendstoInDistribution.tendsto_boundedContinuous_integral {ι : Type u_1} {Ω' : Type u_2} {E : Type u_3} {Ω : ι → Type u_4} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] [SeminormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} {X : (i : ι) → Ω i → E} {Z : Ω' → E} (h : MeasureTheory.TendstoInDistribution X l Z μ μ') (f : BoundedContinuousFunction E ℂ) : Filter.Tendsto (fun (i : ι) => ∫ (x : E), f x ∂MeasureTheory.Measure.map (X i) (μ i)) l (nhds (∫ (x : E), f x ∂MeasureTheory.Measure.map Z μ'))

Weak convergence implies convergence of every bounded continuous complex test integral, over an arbitrary index filter.

theorem Anderson4D.TendstoInDistribution.tendsto_charFun {ι : Type u_1} {Ω' : Type u_2} {E : Type u_3} {Ω : ι → Type u_4} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} {X : (i : ι) → Ω i → E} {Z : Ω' → E} (h : MeasureTheory.TendstoInDistribution X l Z μ μ') (t : E) : Filter.Tendsto (fun (i : ι) => MeasureTheory.charFun (MeasureTheory.Measure.map (X i) (μ i)) t) l (nhds (MeasureTheory.charFun (MeasureTheory.Measure.map Z μ') t))

Filter-indexed forward Lévy implication for convergence in distribution.

theorem Anderson4D.TendstoInDistribution.tendsto_charFun_integral {ι : Type u_1} {Ω' : Type u_2} {E : Type u_3} {Ω : ι → Type u_4} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {l : Filter ι} {X : (i : ι) → Ω i → E} {Z : Ω' → E} (h : MeasureTheory.TendstoInDistribution X l Z μ μ') (t : E) : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω i), Complex.exp (↑(inner ℝ (X i ω) t) * Complex.I) ∂μ i) l (nhds (∫ (ω : Ω'), Complex.exp (↑(inner ℝ (Z ω) t) * Complex.I) ∂μ'))

The same characteristic-function convergence, rewritten as expectations on the original probability spaces.

theorem Anderson4D.TendstoInDistribution.tendsto_real_exp_integral {ι : Type u_1} {Ω' : Type u_2} {Ω : ι → Type u_4} [(i : ι) → MeasurableSpace (Ω i)] (μ : (i : ι) → MeasureTheory.Measure (Ω i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [MeasurableSpace Ω'] (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] {l : Filter ι} {X : (i : ι) → Ω i → ℝ} {Z : Ω' → ℝ} (h : MeasureTheory.TendstoInDistribution X l Z μ μ') : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω i), Complex.exp (Complex.I * ↑(X i ω)) ∂μ i) l (nhds (∫ (ω : Ω'), Complex.exp (Complex.I * ↑(Z ω)) ∂μ'))

Scalar specialization at frequency one, in the exact exponential shape used by paper (3.34).