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

𝔼[Xm]
: conditional expectation ofX
with respect to the measurevolume
and the measurable spacem
. The similarP[Xm]
for a measureP
is defined inMeasureTheory.Function.ConditionalExpectation.Basic
. 
P⟦sm⟧ = 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
andMeasureTheory.ComplexMeasure.rnDeriv
. 
ℙ
is a notation forvolume
on a measured space.
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 "ℙ")