Convergence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compactness and uniqueness of probability limits

Tightness and uniqueness of subsequential limits imply weak convergence, as in the final compactness argument for prime-degree torus packets.

theorem OAI.DukePrimeDegree.tendsto_of_tight_of_unique_subsequential_limit line 21

Source documentation

Tight probability measures converge if every convergent subsequence has the specified limit. Prokhorov compactness ensures that this statement also rules out loss of mass.

theorem tendsto_of_tight_of_unique_subsequential_limit
    {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
    [BorelSpace X] [T2Space X] [FirstCountableTopology (ProbabilityMeasure X)]
    (μ : ℕ → ProbabilityMeasure X) (m : ProbabilityMeasure X)
    (htight : IsTightMeasureSet {ν : Measure X | ∃ i, ν = μ i})
    (hlimit : ∀ (φ : ℕ → ℕ), StrictMono φ → ∀ ν : ProbabilityMeasure X,
      Tendsto (μ ∘ φ) atTop (𝓝 ν) → ν = m) :
    Tendsto μ atTop (𝓝 m) := by
…