Probability measure support lemmas

For a probability measure, 1 - μ sᶜ ≤ μ s for an arbitrary set s.

Mathlib's prob_compl_eq_one_sub₀ requires NullMeasurableSet s and prob_compl_le_one_sub_of_le_prob requires MeasurableSet s; this lemma needs nothing, because subadditivity 1 = μ (s ∪ sᶜ) ≤ μ s + μ sᶜ holds for outer measures. This is the form in which high-probability events are consumed when converting vanishing failure probabilities into convergence statements, where the event sets are often not (easily) measurable.

The zero measure is not a probability measure. The simp lemma for this fact also simplifies totalized distribution laws that reduce to zero outside their parameter range.

Main results

• MeasureTheory.Measure.one_sub_measure_compl_le
• MeasureTheory.not_isProbabilityMeasure_zero
• Finset.norm_prod_measureReal_le_one: a finite product of real masses of a zero-or-probability measure has norm at most one.

Source

The complement bound is adapted from the Davis--Kahan/DKPS formalization, ForMathlib/MeasureTheory/Measure/Typeclasses/Probability.lean at fc38eb4, by Claude Fable 5 (Kitware, Inc., Apache-2.0); the public theorem is exposed in MeasureTheory.Measure.

@[simp]

theorem MeasureTheory.not_isProbabilityMeasure_zero {α : Type u_1} [MeasurableSpace α] : ¬IsProbabilityMeasure 0

The zero measure is not a probability measure. It is a simp lemma so that simp, after rewriting a law to 0 off its parameter range, can still decide IsProbabilityMeasure of that law.

theorem MeasureTheory.Measure.one_sub_measure_compl_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (s : Set Ω) : 1 - μ sᶜ ≤ μ s

For a probability measure, 1 - μ sᶜ ≤ μ s, with no measurability assumption on s: subadditivity gives 1 = μ (s ∪ sᶜ) ≤ μ s + μ sᶜ.

theorem Finset.norm_prod_measureReal_le_one {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (s : Finset ι) (μ : MeasureTheory.Measure α) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (B : ι → Set α) : ‖∏ i ∈ s, μ.real (B i)‖ ≤ 1

A finite product of values of a zero-or-probability measure has norm at most one.