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
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.
The conditional probability measure of any finite measure on any set of positive measure is a probability measure.
The axiomatic definition of conditional probability derived from a measure-theoretic one.
Conditioning first on s and then on t results in the same measure as conditioning
on s ∩ t.
A version of the law of total probability.
Bayes' Theorem