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.

def ProbabilityTheory.«term𝔼[_|_]» : Lean.ParserDescr

Equations

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

def ProbabilityTheory.«term_[_]» : Lean.TrailingParserDescr

Equations

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

def ProbabilityTheory.«term𝔼[_]» : Lean.ParserDescr

Equations

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

def ProbabilityTheory.«term_⟦_|_⟧» : Lean.TrailingParserDescr

Equations

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

def ProbabilityTheory.«term_=ₐₛ_» : Lean.TrailingParserDescr

Equations

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

def ProbabilityTheory.«term_≤ₐₛ_» : Lean.TrailingParserDescr

Equations

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

def ProbabilityTheory.«term∂_/∂_» : Lean.ParserDescr

Equations

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

def ProbabilityTheory.termℙ : Lean.ParserDescr

Equations

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