theorem continuous_finiteMeasure_apply_of_isClopen {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X} (s_clopen : IsClopen s) : Continuous fun (μ : MeasureTheory.FiniteMeasure X) => (↑μ).real s

The measure of any connected component depends continuously on the FiniteMeasure.

theorem continuous_probabilityMeasure_apply_of_isClopen {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] {s : Set X} (s_clopen : IsClopen s) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => (↑μ).real s

The probability of any connected component depends continuously on the ProbabilityMeasure.

theorem continuous_pmf_apply' {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] (i : X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => (↑μ).real {i}

theorem continuous_pmf_apply {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] (i : X) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => μ {i}

theorem tendsto_lintegral_of_forall_of_finite {ι : Type u_1} {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] [Finite X] {L : Filter ι} (μs : ι → MeasureTheory.Measure X) (μ : MeasureTheory.Measure X) (f : BoundedContinuousFunction X NNReal) (h : ∀ (x : X), Filter.Tendsto (fun (i : ι) => (μs i) {x}) L (nhds (μ {x}))) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : X), ↑(f x) ∂μs i) L (nhds (∫⁻ (x : X), ↑(f x) ∂μ))

theorem ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {ι : Type u_1} {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] {L : Filter ι} [Finite X] (μs : ι → MeasureTheory.ProbabilityMeasure X) (μ : MeasureTheory.ProbabilityMeasure X) : Filter.Tendsto μs L (nhds μ) ↔ ∀ (a : X), Filter.Tendsto (fun (x : ι) => (μs x) {a}) L (nhds (μ {a}))

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.

theorem ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal {ι : Type u_1} {X : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [DiscreteTopology X] [BorelSpace X] {L : Filter ι} [Finite X] (μs : ι → MeasureTheory.ProbabilityMeasure X) (μ : MeasureTheory.ProbabilityMeasure X) : Filter.Tendsto μs L (nhds μ) ↔ ∀ (a : X), Filter.Tendsto (fun (n : ι) => ↑(μs n) {a}) L (nhds (↑μ {a}))

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∞.