Constructing and transferring limits in measure

General tools for convergence in measure on finite measures: absolutely continuous and mapped measures, Cauchy completeness, joint fiber limits, uniform approximation, and diagonal extraction.

theorem BGW.Probability.tendstoInMeasure_of_absolutelyContinuous {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ν] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → Ω → ℝ} {g : Ω → ℝ} (hν : ν.AbsolutelyContinuous μ) (hf : ∀ (i : ι), Measurable (f i)) (hconv : MeasureTheory.TendstoInMeasure μ f l g) : MeasureTheory.TendstoInMeasure ν f l g

Convergence in measure transfers to a finite absolutely continuous measure along any countably generated filter.

theorem BGW.Probability.tendstoInMeasure_map_iff {Ω : Type u_1} {Ξ : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ξ] {μ : MeasureTheory.Measure Ω} {p : Ω → Ξ} (hp : Measurable p) {f : ι → Ξ → ℝ} {g : Ξ → ℝ} {l : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) (hg : Measurable g) : MeasureTheory.TendstoInMeasure (MeasureTheory.Measure.map p μ) f l g ↔ MeasureTheory.TendstoInMeasure μ (fun (i : ι) (x : Ω) => f i (p x)) l fun (x : Ω) => g (p x)

Convergence in measure on a pushforward measure is convergence of the composed tests.

theorem BGW.Probability.exists_tendstoInMeasure_of_prefix_absolutelyContinuous {Ω : Type u_1} {Ξ : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ξ] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ν] {p : Ω → Ξ} (hp : Measurable p) {l : Filter ι} [l.IsCountablyGenerated] [l.NeBot] {f : ι → Ξ → ℝ} {g : Ω → ℝ} (hf : ∀ (i : ι), Measurable (f i)) (hconv : MeasureTheory.TendstoInMeasure μ (fun (i : ι) (x : Ω) => f i (p x)) l g) (hν : (MeasureTheory.Measure.map p ν).AbsolutelyContinuous (MeasureTheory.Measure.map p μ)) : ∃ (L : Ω → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure ν (fun (i : ι) (x : Ω) => f i (p x)) l L

Existence of a measurable limit transfers through absolutely continuous prefix laws. The original limit need not have been chosen as a function of the prefix.

theorem BGW.Probability.exists_tendstoInMeasure_of_cauchy {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {l : Filter ι} [l.NeBot] {f : ι → Ω → ℝ} (hf : ∀ (i : ι), Measurable (f i)) (hc : ∀ (δ : ℝ), 0 < δ → ∀ (η : ENNReal), 0 < η → ∃ S ∈ l, ∀ i ∈ S, ∀ j ∈ S, μ {x : Ω | δ ≤ dist (f i x) (f j x)} ≤ η) : ∃ (L : Ω → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure μ f l L

A measurable real Cauchy family in a finite measure space has a measurable limit in measure.

theorem BGW.Probability.tendstoInMeasure_cauchy {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {l : Filter ι} {F : ι → Ω → ℝ} {L : Ω → ℝ} (h : MeasureTheory.TendstoInMeasure μ F l L) (δ : ℝ) (hδ : 0 < δ) (η : ENNReal) (hη : 0 < η) : ∃ A ∈ l, ∀ i ∈ A, ∀ j ∈ A, μ {x : Ω | δ ≤ dist (F i x) (F j x)} ≤ η

A convergent family satisfies the uniform-set Cauchy criterion in measure.

theorem BGW.Probability.exists_joint_tendstoInMeasure_of_fiber_limits {A : Type u_1} {Ω : Type u_2} {ι : Type u_3} [MeasurableSpace A] [MeasurableSpace Ω] (ν : MeasureTheory.Measure A) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] {S : Set (A × Ω)} (hS : MeasurableSet S) [MeasureTheory.IsFiniteMeasure ((ν.prod μ).restrict S)] {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] (F : ι → A × Ω → ℝ) (hF : ∀ (i : ι), Measurable (F i)) (hlim : ∀ᵐ (s : A) ∂ν, ∃ (L : Ω → ℝ), MeasureTheory.TendstoInMeasure (μ.restrict {x : Ω | (s, x) ∈ S}) (fun (i : ι) (x : Ω) => F i (s, x)) l L) : ∃ (L : A × Ω → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure ((ν.prod μ).restrict S) F l L

Fiberwise convergence gives a jointly measurable limit on a finite restriction of a product measure. No measurable choice of the individual fiber limits is assumed.

theorem BGW.Probability.exists_tendstoInMeasure_of_uniform_approximation {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (F : ℝ → Ω → ℝ) (G : ℕ → ℝ → Ω → ℝ) (L : ℕ → Ω → ℝ) (b : ℕ → ENNReal) (hF : ∀ (ε : ℝ), Measurable (F ε)) (hG : ∀ (n : ℕ) (ε : ℝ), Measurable (G n ε)) (hconv : ∀ (n : ℕ), MeasureTheory.TendstoInMeasure μ (G n) (nhdsWithin 0 (Set.Ioi 0)) (L n)) (hb : Filter.Tendsto b Filter.atTop (nhds 0)) (herr : ∀ (n : ℕ) (ε : ℝ), 0 < ε → ∫⁻ (x : Ω), ENNReal.ofReal (dist (F ε x) (G n ε x)) ∂μ ≤ b n) : ∃ (H : Ω → ℝ), Measurable H ∧ MeasureTheory.TendstoInMeasure μ F (nhdsWithin 0 (Set.Ioi 0)) H

A real family uniformly approximated in first moment by convergent families has a measurable limit in measure.

theorem BGW.Probability.exists_diagonal_subseq {ι : Type u_1} [Countable ι] (Good : ι → (ℕ → ℕ) → Prop) (htail : ∀ (i : ι) (φ ψ : ℕ → ℕ), StrictMono φ → StrictMono ψ → (∃ (N : ℕ), ∀ k ≥ N, ∃ (j : ℕ), ψ k = φ j) → Good i φ → Good i ψ) (hext : ∀ (i : ι) (φ : ℕ → ℕ), StrictMono φ → ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ Good i (φ ∘ ψ)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (i : ι), Good i φ

Countably many extractable predicates, inherited by eventual subsequences, have one common strictly increasing subsequence.

theorem BGW.Probability.tendstoInMeasure_continuous_comp_filter {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {l : Filter ι} [l.IsCountablyGenerated] {f : ι → Ω → ℝ} {g : Ω → ℝ} (hf : ∀ (i : ι), Measurable (f i)) (hg : MeasureTheory.TendstoInMeasure μ f l g) {φ : ℝ → ℝ} (hφ : Continuous φ) : MeasureTheory.TendstoInMeasure μ (fun (i : ι) (ω : Ω) => φ (f i ω)) l fun (ω : Ω) => φ (g ω)

Continuous real tests preserve convergence in measure along a countably generated filter.