# mathlib3documentation

probability.conditional_probability

# Conditional Probability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 probability_theory.

## 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

noncomputable def probability_theory.cond {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) (s : set Ω) :

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
theorem probability_theory.cond_is_probability_measure {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s : set Ω} (hcs : μ s 0) :

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

@[simp]
@[simp]
theorem probability_theory.cond_univ {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω)  :
theorem probability_theory.cond_apply {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s : set Ω} (hms : measurable_set s) (t : set Ω) :
t = (μ s)⁻¹ * μ (s t)

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

theorem probability_theory.cond_inter_self {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s : set Ω} (hms : measurable_set s) (t : set Ω) :
(s t) = t
theorem probability_theory.inter_pos_of_cond_ne_zero {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hcst : t 0) :
0 < μ (s t)
theorem probability_theory.cond_pos_of_inter_ne_zero {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hci : μ (s t) 0) :
0 < t
theorem probability_theory.cond_cond_eq_cond_inter' {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hmt : measurable_set t) (hcs : μ s ) (hci : μ (s t) 0) :
= (s t)
theorem probability_theory.cond_cond_eq_cond_inter {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hmt : measurable_set t) (hci : μ (s t) 0) :
= (s t)

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

theorem probability_theory.cond_mul_eq_inter' {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s : set Ω} (hms : measurable_set s) (hcs : μ s 0) (hcs' : μ s ) (t : set Ω) :
t * μ s = μ (s t)
theorem probability_theory.cond_mul_eq_inter {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s : set Ω} (hms : measurable_set s) (hcs : μ s 0) (t : set Ω) :
t * μ s = μ (s t)
theorem probability_theory.cond_add_cond_compl_eq {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hcs : μ s 0) (hcs' : μ s 0) :
t * μ s + t * μ s = μ t

A version of the law of total probability.

theorem probability_theory.cond_eq_inv_mul_cond_mul {Ω : Type u_1} {m : measurable_space Ω} (μ : measure_theory.measure Ω) {s t : set Ω} (hms : measurable_set s) (hmt : measurable_set t) :
t = (μ s)⁻¹ * s * μ t

Bayes' Theorem