Classes for probability measures #
We introduce the following typeclasses for measures:
IsZeroOrProbabilityMeasure μ:μ univ = 0 ∨ μ univ = 1;IsProbabilityMeasure μ:μ univ = 1.
class
MeasureTheory.IsZeroOrProbabilityMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
:
A measure μ is zero or a probability measure if μ univ = 0 or μ univ = 1. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.
Instances
theorem
MeasureTheory.isZeroOrProbabilityMeasure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
theorem
MeasureTheory.prob_le_one
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
{s : Set α}
:
theorem
MeasureTheory.measureReal_le_one
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
{s : Set α}
:
@[deprecated MeasureTheory.measureReal_le_one (since := "2025-04-19")]
theorem
MeasureTheory.toReal_prob_le_one
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
{s : Set α}
:
Alias of MeasureTheory.measureReal_le_one.
@[simp]
theorem
MeasureTheory.one_le_prob_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
:
@[instance 100]
instance
MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsZeroOrProbabilityMeasure μ]
:
instance
MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
:
A measure μ is called a probability measure if μ univ = 1.
Instances
theorem
MeasureTheory.isProbabilityMeasure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
@[instance 100]
instance
MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.IsProbabilityMeasure.ne_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsProbabilityMeasure μ]
:
@[instance 100]
instance
MeasureTheory.IsProbabilityMeasure.neZero
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsProbabilityMeasure μ]
:
NeZero μ
theorem
MeasureTheory.IsProbabilityMeasure.ae_neBot
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.prob_add_prob_compl
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(h : MeasurableSet s)
:
instance
MeasureTheory.isProbabilityMeasureSMul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
[NeZero μ]
:
IsProbabilityMeasure ((μ Set.univ)⁻¹ • μ)
theorem
MeasureTheory.Measure.isProbabilityMeasure_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
[IsProbabilityMeasure μ]
{f : α → β}
(hf : AEMeasurable f μ)
:
IsProbabilityMeasure (map f μ)
theorem
MeasureTheory.Measure.isProbabilityMeasure_of_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
[IsProbabilityMeasure (map f μ)]
:
theorem
MeasureTheory.Measure.isProbabilityMeasure_map_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
instance
MeasureTheory.IsProbabilityMeasure_comap_equiv
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
[IsProbabilityMeasure μ]
(f : β ≃ᵐ α)
:
IsProbabilityMeasure (Measure.comap (⇑f) μ)
theorem
MeasureTheory.prob_compl_eq_one_sub₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(h : NullMeasurableSet s μ)
:
Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞.
Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the
better-behaved subtraction of ℝ.
theorem
MeasureTheory.prob_compl_eq_one_sub
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : MeasurableSet s)
:
Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞.
Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the
better-behaved subtraction of ℝ.
@[simp]
theorem
MeasureTheory.prob_compl_eq_zero_iff₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : NullMeasurableSet s μ)
:
theorem
MeasureTheory.prob_compl_eq_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.prob_compl_eq_one_iff₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : NullMeasurableSet s μ)
:
theorem
MeasureTheory.prob_compl_eq_one_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : MeasurableSet s)
:
theorem
MeasureTheory.mem_ae_iff_prob_eq_one₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : NullMeasurableSet s μ)
:
theorem
MeasureTheory.mem_ae_iff_prob_eq_one
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsProbabilityMeasure μ]
(hs : MeasurableSet s)
:
theorem
MeasureTheory.ae_iff_prob_eq_one
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsProbabilityMeasure μ]
{p : α → Prop}
(hp : Measurable p)
:
theorem
MeasureTheory.isProbabilityMeasure_comap
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
[IsProbabilityMeasure μ]
{f : β → α}
(hf : Function.Injective f)
(hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f)
(hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s))
:
theorem
MeasurableEmbedding.isProbabilityMeasure_comap
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
{f : β → α}
(hf : MeasurableEmbedding f)
(hf' : ∀ᵐ (a : α) ∂μ, a ∈ Set.range f)
:
instance
MeasureTheory.isProbabilityMeasure_map_up
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsProbabilityMeasure μ]
:
instance
MeasureTheory.isProbabilityMeasure_comap_down
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.Measure.eq_of_le_of_isProbabilityMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : Measure α}
[IsProbabilityMeasure μ]
[IsProbabilityMeasure ν]
(hμν : μ ≤ ν)
:
instance
MeasureTheory.isZeroOrProbabilityMeasureSMul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
:
IsZeroOrProbabilityMeasure ((μ Set.univ)⁻¹ • μ)
theorem
MeasureTheory.eq_zero_or_isProbabilityMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : Measure α)
[IsZeroOrProbabilityMeasure μ]
:
instance
MeasureTheory.instIsZeroOrProbabilityMeasureMap
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
{f : α → β}
:
theorem
MeasureTheory.prob_compl_lt_one_sub_of_lt_prob
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsZeroOrProbabilityMeasure μ]
{p : ENNReal}
(hμs : p < μ s)
(s_mble : MeasurableSet s)
:
theorem
MeasureTheory.prob_compl_le_one_sub_of_le_prob
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
{s : Set α}
[IsZeroOrProbabilityMeasure μ]
{p : ENNReal}
(hμs : p ≤ μ s)
(s_mble : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.inv_measure_univ_smul_eq_self
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : Measure α}
[IsZeroOrProbabilityMeasure μ]
: