Conditional Probability

This file defines conditional probability and includes basic results relating to it.

Given some measure μ defined on a measure space on some type Ω and some s : Set Ω, we define the measure of μ conditioned on s as the restricted measure scaled by the inverse of the measure of s: cond μ s = (μ s)⁻¹ • μ.restrict s. The scaling ensures that this is a probability measure (when μ is a finite measure).

From this definition, we derive the "axiomatic" definition of conditional probability based on application: for any s t : Set Ω, we have μ[t|s] = (μ s)⁻¹ * μ (s ∩ t).

Main Statements

• cond_cond_eq_cond_inter: conditioning on one set and then another is equivalent to conditioning on their intersection.
• cond_eq_inv_mul_cond_mul: Bayes' Theorem, μ[t|s] = (μ s)⁻¹ * μ[s|t] * (μ t).

Notations

This file uses the notation μ[|s] the measure of μ conditioned on s, and μ[t|s] for the probability of t given s under μ (equivalent to the application μ[|s] t).

These notations are contained in the locale ProbabilityTheory.

Implementation notes

Because we have the alternative measure restriction application principles Measure.restrict_apply and Measure.restrict_apply', which require measurability of the restricted and restricting sets, respectively, many of the theorems here will have corresponding alternatives as well. For the sake of brevity, we've chosen to only go with Measure.restrict_apply' for now, but the alternative theorems can be added if needed.

Use of @[simp] generally follows the rule of removing conditions on a measure when possible.

Hypotheses that are used to "define" a conditional distribution by requiring that the conditioning set has non-zero measure should be named using the abbreviation "c" (which stands for "conditionable") rather than "nz". For example (hci : μ (s ∩ t) ≠ 0) (rather than hnzi) should be used for a hypothesis ensuring that μ[|s ∩ t] is defined.

Tags

conditional, conditioned, bayes

def ProbabilityTheory.cond {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (s : Set Ω) : MeasureTheory.Measure Ω

The conditional probability measure of measure μ on set s is μ restricted to s and scaled by the inverse of μ s (to make it a probability measure): (μ s)⁻¹ • μ.restrict s.

Equations

• ProbabilityTheory.cond μ s = (μ s)⁻¹ • μ.restrict s

def ProbabilityTheory.«term_[_|_]» : Lean.TrailingParserDescr

The conditional probability measure of measure μ on set s is μ restricted to s and scaled by the inverse of μ s (to make it a probability measure): (μ s)⁻¹ • μ.restrict s.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«term_[|_]» : Lean.TrailingParserDescr

The conditional probability measure of measure μ on set s is μ restricted to s and scaled by the inverse of μ s (to make it a probability measure): (μ s)⁻¹ • μ.restrict s.

Equations

• One or more equations did not get rendered due to their size.

def ProbabilityTheory.«term_[|_←_]» : Lean.TrailingParserDescr

The conditional probability measure of measure μ on {ω | X ω = x}.

It is μ restricted to {ω | X ω = x} and scaled by the inverse of μ {ω | X ω = x} (to make it a probability measure): (μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.cond_isProbabilityMeasure_of_finite {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hcs : μ s ≠ 0) (hs : μ s ≠ ⊤) : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cond μ s)

The conditional probability measure of any measure on any set of finite positive measure is a probability measure.

theorem ProbabilityTheory.cond_isProbabilityMeasure {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hcs : μ s ≠ 0) : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cond μ s)

The conditional probability measure of any finite measure on any set of positive measure is a probability measure.

instance ProbabilityTheory.instIsZeroOrProbabilityMeasureCond {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} : MeasureTheory.IsZeroOrProbabilityMeasure (ProbabilityTheory.cond μ s)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.cond_toMeasurable_eq {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s : Set Ω} : ProbabilityTheory.cond μ (MeasureTheory.toMeasurable μ s) = ProbabilityTheory.cond μ s

theorem ProbabilityTheory.cond_absolutelyContinuous {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} : (ProbabilityTheory.cond μ s).AbsolutelyContinuous μ

theorem ProbabilityTheory.absolutelyContinuous_cond_univ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : μ.AbsolutelyContinuous (ProbabilityTheory.cond μ Set.univ)

@[simp]

theorem ProbabilityTheory.cond_empty {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) : ProbabilityTheory.cond μ ∅ = 0

@[simp]

theorem ProbabilityTheory.cond_univ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.cond μ Set.univ = μ

@[simp]

theorem ProbabilityTheory.cond_eq_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hμs : μ s ≠ ⊤) : ProbabilityTheory.cond μ s = 0 ↔ μ s = 0

theorem ProbabilityTheory.cond_eq_zero_of_meas_eq_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hμs : μ s = 0) : ProbabilityTheory.cond μ s = 0

theorem ProbabilityTheory.cond_apply {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} (hms : MeasurableSet s) (μ : MeasureTheory.Measure Ω) (t : Set Ω) : (ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * μ (s ∩ t)

The axiomatic definition of conditional probability derived from a measure-theoretic one.

theorem ProbabilityTheory.cond_apply' {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} (ht : MeasurableSet t) (μ : MeasureTheory.Measure Ω) : (ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * μ (s ∩ t)

@[simp]

theorem ProbabilityTheory.cond_apply_self {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ⊤) : (ProbabilityTheory.cond μ s) s = 1

theorem ProbabilityTheory.cond_inter_self {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} (hms : MeasurableSet s) (t : Set Ω) (μ : MeasureTheory.Measure Ω) : (ProbabilityTheory.cond μ s) (s ∩ t) = (ProbabilityTheory.cond μ s) t

theorem ProbabilityTheory.inter_pos_of_cond_ne_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} {t : Set Ω} (hms : MeasurableSet s) (hcst : (ProbabilityTheory.cond μ s) t ≠ 0) : 0 < μ (s ∩ t)

theorem ProbabilityTheory.cond_pos_of_inter_ne_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} {t : Set Ω} [MeasureTheory.IsFiniteMeasure μ] (hms : MeasurableSet s) (hci : μ (s ∩ t) ≠ 0) : 0 < (ProbabilityTheory.cond μ s) t

theorem ProbabilityTheory.cond_cond_eq_cond_inter' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} {t : Set Ω} (hms : MeasurableSet s) (hmt : MeasurableSet t) (hcs : μ s ≠ ⊤) : ProbabilityTheory.cond (ProbabilityTheory.cond μ s) t = ProbabilityTheory.cond μ (s ∩ t)

theorem ProbabilityTheory.cond_cond_eq_cond_inter {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.cond (ProbabilityTheory.cond μ s) t = ProbabilityTheory.cond μ (s ∩ t)

Conditioning first on s and then on t results in the same measure as conditioning on s ∩ t.

theorem ProbabilityTheory.cond_mul_eq_inter' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hms : MeasurableSet s) (hcs' : μ s ≠ ⊤) (t : Set Ω) : (ProbabilityTheory.cond μ s) t * μ s = μ (s ∩ t)

theorem ProbabilityTheory.cond_mul_eq_inter {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} (hms : MeasurableSet s) (t : Set Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (ProbabilityTheory.cond μ s) t * μ s = μ (s ∩ t)

theorem ProbabilityTheory.cond_add_cond_compl_eq {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} (hms : MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (ProbabilityTheory.cond μ s) t * μ s + (ProbabilityTheory.cond μ sᶜ) t * μ sᶜ = μ t

A version of the law of total probability.

theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {s : Set Ω} {t : Set Ω} (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : (ProbabilityTheory.cond μ s) t = (μ s)⁻¹ * (ProbabilityTheory.cond μ t) s * μ t

Bayes' Theorem

theorem ProbabilityTheory.comap_cond {Ω : Type u_1} {Ω' : Type u_2} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω} {s : Set Ω} {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ (ω : Ω) ∂μ, ω ∈ Set.range i) (hs : MeasurableSet s) : MeasureTheory.Measure.comap i (ProbabilityTheory.cond μ s) = ProbabilityTheory.cond (MeasureTheory.Measure.comap i μ) (i ⁻¹' s)

theorem ProbabilityTheory.sum_meas_smul_cond_fiber {Ω : Type u_1} {α : Type u_3} {m : MeasurableSpace Ω} [Fintype α] [MeasurableSpace α] [DiscreteMeasurableSpace α] {X : Ω → α} (hX : Measurable X) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ∑ x : α, μ (X ⁻¹' {x}) • ProbabilityTheory.cond μ (X ⁻¹' {x}) = μ

The law of total probability for a random variable taking finitely many values: a measure μ can be expressed as a linear combination of its conditional measures μ[|X ← x] on fibers of a random variable X valued in a fintype.