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
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).
This file uses the notation
μ[|s] the measure of
μ conditioned on
μ[t|s] for the probability of
μ (equivalent to the
These notations are contained in the locale
Implementation notes #
Because we have the alternative measure restriction application principles
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
for now, but the alternative theorems can be added if needed.
@[simp] generally follows the rule of removing conditions on a measure
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)
hnzi) should be used for a hypothesis ensuring that
μ[|s ∩ t] is defined.
conditional, conditioned, bayes
The conditional probability measure of measure
μ on set
μ restricted to
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
s ∩ t.
A version of the law of total probability.