ErgodicMixtureLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded limits through the published ergodic decomposition

Setwise barycenters are enough for the stationary-increment application. No measurable selection of a label on the components is needed.

theorem OAI.PolycyclicRecognition.lintegral_eq_of_setwise_barycenter line 21

Source documentation

Extend a setwise decomposition to every nonnegative measurable integrand.

theorem lintegral_eq_of_setwise_barycenter (μ : Measure X) (κ : X → Measure X)
    (hκ : ∀ s : Set X, MeasurableSet s → Measurable (fun x => κ x s))
    (hbary : ∀ s : Set X, MeasurableSet s → μ s = ∫⁻ x, κ x s ∂μ)
    (f : X → ℝ≥0∞) (hf : Measurable f) :
    ∫⁻ x, f x ∂μ = ∫⁻ x, ∫⁻ y, f y ∂κ x ∂μ := by
…

theorem OAI.PolycyclicRecognition.tendsto_lintegral_of_componentwise_bounded line 34

Source documentation

Uniformly bounded componentwise convergence passes through a probability barycenter, with the component map kept fixed throughout the limit.

theorem tendsto_lintegral_of_componentwise_bounded
    (μ : Measure X) [IsProbabilityMeasure μ] (κ : X → Measure X)
    (hκ : ∀ s : Set X, MeasurableSet s → Measurable (fun x => κ x s))
    (hbary : ∀ s : Set X, MeasurableSet s → μ s = ∫⁻ x, κ x s ∂μ)
    {ι : Type*} {l : Filter ι} [l.IsCountablyGenerated]
    (f : ι → X → ℝ≥0∞) (hf : ∀ n, Measurable (f n))
    {B : ℝ≥0∞} (hB : B ≠ ⊤)
    (hbound : ∀ᶠ n in l, ∀ x, ∫⁻ y, f n y ∂κ x ≤ B)
    (hlim : ∀ x, Tendsto (fun n => ∫⁻ y, f n y ∂κ x) l (𝓝 0)) :
    Tendsto (fun n => ∫⁻ x, f n x ∂μ) l (𝓝 0) := by
…