instance instCanLiftMeasureProbabilityMeasureToMeasureIsProbabilityMeasure_pFR {Y : Type u_1} [MeasurableSpace Y] :
A Measure which is a probability measure can be lifted to a ProbabilityMeasure.
instance instCanLiftMeasureFiniteMeasureToMeasureIsFiniteMeasure_pFR {Y : Type u_1} [MeasurableSpace Y] :
A Measure which is a finite measure can be lifted to a FiniteMeasure.
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}))) :
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∞.