Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityMeasure.tendsto_iff_forall_apply_tendsto

PFR.Mathlib.MeasureTheory.Measure.ProbabilityMeasure · PFR/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean:64 to 76

Source documentation

Probability measures on a finite space tend to a limit if and only if the probability masses of all points tend to the corresponding limits. Version in ℝ≥0.

Exact Lean statement

lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {L : Filter ι} [Finite X]
    (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X) :
    Tendsto μs L (𝓝 μ) ↔ ∀ a, Tendsto (μs · {a}) L (𝓝 (μ {a}))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {L : Filter ι} [Finite X]    (μs : ι → ProbabilityMeasure X) (μ : ProbabilityMeasure X) :    Tendsto μs L (𝓝 μ) ↔ ∀ a, Tendsto (μs · {a}) L (𝓝 (μ {a})) := by  constructor <;> intro h  · exact fun a ↦ ((continuous_pmf_apply a).continuousAt (x := μ)).tendsto.comp h  · apply ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr    intro f    apply tendsto_lintegral_of_forall_of_finite    intro a    -- TODO: rename `ENNReal.continuous_coe` to `ENNReal.continuous_ofNNReal`?    convert ENNReal.continuous_coe.continuousAt.tendsto.comp (h a)    · simp [Function.comp_apply, ennreal_coeFn_eq_coeFn_toMeasure]    · simp [ennreal_coeFn_eq_coeFn_toMeasure]