# 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

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

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

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

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

## Equations

- ⋯ = ⋯

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

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.