OAI/Analysis/FiniteFactor/FiniteMeasureCylinderCriterion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.finiteMeasure_tendsto_of_piSystem line 12

   Source documentation

   Finite-measure version of the neighborhood pi-system criterion. Total mass convergence is required; zero limiting mass is handled separately.

   theorem finiteMeasure_tendsto_of_piSystem {Ω : Type*} [MeasurableSpace Ω]
       [TopologicalSpace Ω] [SecondCountableTopology Ω] [OpensMeasurableSpace Ω]
       [Nonempty Ω] {S : Set (Set Ω)} (hS : IsPiSystem S)
       {μ : ℕ → FiniteMeasure Ω} {ν : FiniteMeasure Ω}
       (hmeas : ∀ s ∈ S, MeasurableSet s)
       (hbasis : ∀ u : Set Ω, IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u)
       (hmass : Tendsto (fun n => (μ n).mass) atTop (𝓝 ν.mass))
       (hsets : ∀ s ∈ S, Tendsto (fun n => μ n s) atTop (𝓝 (ν s))) :
       Tendsto μ atTop (𝓝 ν) := by
   …