# Notations for probability theory #

This file defines the following notations, for functions `X,Y`

, measures `P, Q`

defined on a
measurable space `m0`

, and another measurable space structure `m`

with `hm : m ≤ m0`

,

`P[X] = ∫ a, X a ∂P`

`𝔼[X] = ∫ a, X a`

`𝔼[X|m]`

: conditional expectation of`X`

with respect to the measure`volume`

and the measurable space`m`

. The similar`P[X|m]`

for a measure`P`

is defined in`MeasureTheory.Function.ConditionalExpectation.Basic`

.`P⟦s|m⟧ = P[s.indicator (fun ω => (1 : ℝ)) | m]`

, conditional probability of a set.`X =ₐₛ Y`

:`X =ᵐ[volume] Y`

`X ≤ₐₛ Y`

:`X ≤ᵐ[volume] Y`

`∂P/∂Q = P.rnDeriv Q`

We note that the notation`∂P/∂Q`

applies to three different cases, namely,`MeasureTheory.Measure.rnDeriv`

,`MeasureTheory.SignedMeasure.rnDeriv`

and`MeasureTheory.ComplexMeasure.rnDeriv`

.`ℙ`

is a notation for`volume`

on a measured space.

To use these notations, you need to use `open scoped ProbabilityTheory`

or `open ProbabilityTheory`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

- ProbabilityTheory.termℙ = Lean.ParserDescr.node `ProbabilityTheory.termℙ 1024 (Lean.ParserDescr.symbol "ℙ")