Definitions in probability theory

ClassProbability measure#

A measure μ is called a probability measure if μ univ = 1.

MeasureTheory.IsProbabilityMeasure.{u_1} {α : Type u_1} {m0 : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) : Prop
Sources
MathlibMeasureTheory.IsProbabilityMeasure
Uses 1 · Used by 16
Statement usesPositive measure
Used byThe Ballot Problem · Fourier Series · Jensen's inequality (integral version) · Central limit theorem · Convergence in distribution · Strong law of large numbers · Binomial law · Kolmogorov's \(0\)-\(1\) law · Mean of product of independent random variables · Fernique's theorem · Prokhorov's theorem · Continuous mapping theorem · Ionescu-Tulcea theorem · Lévy continuity theorem · Slutsky's theorem · Borel-Cantelli lemma (difficult direction)

DefinitionIndependent events#

A family of sets is independent if the family of measurable space structures they generate is independent. For a set s, the generated measurable space has measurable sets ∅, s, sᶜ, univ.

ProbabilityTheory.iIndepSet.{u_1, u_2} {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω}
  (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω := by volume_tac) : Prop
Sources
MathlibProbabilityTheory.iIndepSet
Uses 4 · Used by 1
Statement usesAlmost sure convergence · Carathéodory's theorem (measure theory) · Giry monad · Measurable function
Used byBorel-Cantelli lemma (difficult direction)

DefinitionIndependent sigma-algebras#

A family of measurable space structures (i.e. of σ-algebras) is independent with respect to a measure μ (typically defined on a finer σ-algebra) if the family of sets of measurable sets they define is independent. m : ι → MeasurableSpace Ω is independent with respect to measure μ if for any finite set of indices s = {i_1, ..., i_n}, for any sets f i_1 ∈ m i_1, ..., f i_n ∈ m i_n, then μ (⋂ i in s, f i) = ∏ i ∈ s, μ (f i).

ProbabilityTheory.iIndep.{u_1, u_2} {Ω : Type u_1} {ι : Type u_2} (m : ι → MeasurableSpace Ω)
  {_mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω := by volume_tac) : Prop
Sources
MathlibProbabilityTheory.iIndep
Uses 4 · Used by 2
Statement usesAlmost sure convergence · Carathéodory's theorem (measure theory) · Giry monad · Measurable function
Used byKolmogorov's \(0\)-\(1\) law · Borel-Cantelli lemma (difficult direction)

DefinitionConditional probability#

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.

ProbabilityTheory.cond.{u_1} {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω)
  (s : Set Ω) : MeasureTheory.Measure Ω
Sources
MathlibProbabilityTheory.cond
Uses 4 · Used by 4
Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Linear map · Positive measure
Used byThe Ballot Problem · Buffon Needle Problem · The Birthday Problem · Bayes' theorem

DefinitionConditional expectation#

Conditional expectation of a function, with notation μ[f | m].

It is defined as 0 if any one of the following conditions is true: - m is not a sub-σ-algebra of m₀, - μ is not σ-finite with respect to m, - f is not integrable.

MeasureTheory.condExp.{u_1, u_3} {α : Type u_1} {E : Type u_3} (m : MeasurableSpace α)
  {m₀ : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α)
  (f : α → E) : α → E
Sources
MathlibMeasureTheory.condExp
Uses 9 · Used by 3
Statement usesCarathéodory's theorem (measure theory) · Completeness of R · Extension by continuity · Inner product space \(L^2\) · Lipschitz continuity · Norm of a continuous linear map · Orthogonal projection · Topological module · Vector-valued integrable function (Bochner integral)
Used byMartingale · Optional stopping theorem · Borel-Cantelli lemma (difficult direction)

DefinitionCharacteristic function#

The characteristic function of a measure in an inner product space.

MeasureTheory.charFun.{u_2} {E : Type u_2} {mE : MeasurableSpace E} [Inner ℝ E]
  (μ : MeasureTheory.Measure E) (t : E) : ℂ
Sources
MathlibMeasureTheory.charFun
Uses 3 · Used by 1
Statement usesBochner integral · Complex exponential · Inner product space, over \(R\) or \(C\)
Used byLévy continuity theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.