Continuity of products of probability measures on finite types

theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_apply_tendsto {ι : Type u_1} {α : Type u_2} {L : Filter ι} [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α] (μs : ι → MeasureTheory.ProbabilityMeasure α) (μ : MeasureTheory.ProbabilityMeasure α) : Filter.Tendsto μs L (nhds μ) ↔ ∀ (a : α), 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 MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_apply_tendsto_ennreal {ι : Type u_1} {α : Type u_2} {L : Filter ι} [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α] (μs : ι → MeasureTheory.ProbabilityMeasure α) (μ : MeasureTheory.ProbabilityMeasure α) : Filter.Tendsto μs L (nhds μ) ↔ ∀ (a : α), 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∞.

theorem MeasureTheory.ProbabilityMeasure.tendsto_prod_of_tendsto_of_tendsto {ι : Type u_1} {L : Filter ι} {α : Type u_2} {β : Type u_3} [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α] [Finite β] [TopologicalSpace β] [DiscreteTopology β] [MeasurableSpace β] [BorelSpace β] (μs : ι → MeasureTheory.ProbabilityMeasure α) (μ : MeasureTheory.ProbabilityMeasure α) (μs_lim : Filter.Tendsto μs L (nhds μ)) (νs : ι → MeasureTheory.ProbabilityMeasure β) (ν : MeasureTheory.ProbabilityMeasure β) (νs_lim : Filter.Tendsto νs L (nhds ν)) : Filter.Tendsto (fun (i : ι) => (μs i).prod (νs i)) L (nhds (μ.prod ν))

If probability measures on two finite spaces tend to limits, then the products of them on the product space tend to the product of the limits. TODO: In Mathlib, this should be done on all separable metrizable spaces.

instance MeasureTheory.t1Space_probabilityMeasure_of_finite {α : Type u_1} [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α] : T1Space (MeasureTheory.ProbabilityMeasure α)

Equations

• ⋯ = ⋯

theorem MeasureTheory.ProbabilityMeasure.continuous_prod_of_finite {α : Type u_1} {β : Type u_2} [Finite α] [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] [BorelSpace α] [Finite β] [TopologicalSpace β] [DiscreteTopology β] [MeasurableSpace β] [BorelSpace β] : Continuous fun (m : MeasureTheory.ProbabilityMeasure α × MeasureTheory.ProbabilityMeasure β) => m.1.prod m.2

The product of two probability measures on finite spaces depend continuously on the two probability measures. TODO: In Mathlib, this should be done on all separable metrizable spaces.