Random variables and their laws

DefinitionDiscrete law#

A probability mass function, or discrete probability measures is a function α → ℝ≥0∞ such that the values have (infinite) sum 1.

PMF.{u} (α : Type u) : Type u
Sources
MathlibPMF
Uses 2
Statement usesInfinite sum · Real number

ClassProbability density function#

A random variable X : Ω → E is said to have a probability density function (HasPDF) with respect to the measure ℙ on Ω and μ on E if the push-forward measure of ℙ along X is absolutely continuous with respect to μ and they have a Lebesgue decomposition (HaveLebesgueDecomposition).

MeasureTheory.HasPDF.{u_1, u_2} {Ω : Type u_1} {E : Type u_2} [MeasurableSpace E]
  {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : MeasureTheory.Measure Ω)
  (μ : MeasureTheory.Measure E := by volume_tac) : Prop
Sources
MathlibMeasureTheory.HasPDF
Uses 6
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Integral of positive measurable functions · Linear map · Measurable function

DefinitionVariance of a real-valued random variable#

The ℝ-valued variance of a real-valued random variable defined by applying ENNReal.toReal to evariance.

ProbabilityTheory.variance.{u_1} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) : ℝ
Sources
MathlibProbabilityTheory.variance
Uses 2 · Used by 3
Statement usesBochner integral · Inner product space, over \(R\) or \(C\)
Used byCentral limit theorem · Chebyshev inequality · Gaussian measures

DefinitionIndependence of random variables#

A family of functions defined on the same space Ω and taking values in possibly different spaces, each with a measurable space structure, is independent if the family of measurable space structures they generate on Ω is independent. For a function g with codomain having measurable space structure m, the generated measurable space structure is MeasurableSpace.comap g m.

ProbabilityTheory.iIndepFun.{u_1, u_2, u_6} {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω}
  {β : ι → Type u_6} [m : (x : ι) → MeasurableSpace (β x)] (f : (x : ι) → Ω → β x)
  (μ : MeasureTheory.Measure Ω := by volume_tac) : Prop
Sources
MathlibProbabilityTheory.iIndepFun
Uses 4 · Used by 2
Statement usesAlmost sure convergence · Carathéodory's theorem (measure theory) · Giry monad · Measurable function
Used byCentral limit theorem · Borel-Cantelli lemma (difficult direction)

TheoremKolmogorov's \(0\)-\(1\) law#

Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1. The tail σ-algebra limsup s atTop is the same as ⋂ n, ⋃ i ≥ n, s i.

ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop.{u_2, u_3} {Ω : Type u_2}
  {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0)
  (h_indep : ProbabilityTheory.iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet t) :
  μ t = 0 ∨ μ t = 1
Sources
MathlibProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop
Uses 5
Statement usesIndependent sigma-algebras
Proof usesBorel sigma-algebra · Completeness · Metric space · Probability measure

TheoremMean of product of independent random variables#

Mathlib states this as ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral.

ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral.{u_1, u_2} {Ω : Type u_1} {𝕜 : Type u_2}
  [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜}
  (hXY : ProbabilityTheory.IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ)
  (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
  ∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
Sources
MathlibProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
Uses 10
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Giry monad · Inner product space, over \(R\) or \(C\) · Measurable function
Proof usesAlgebra of endomorphisms of a vector space · Characteristic zero · Fubini's theorem · Probability measure · Topology on a normed vector space

DefinitionMoment of a random variable#

Moment of a real random variable, μ[X ^ p].

ProbabilityTheory.moment.{u_1} {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (p : ℕ)
  (μ : MeasureTheory.Measure Ω) : ℝ
Sources
MathlibProbabilityTheory.moment
Uses 2
Statement usesBochner integral · Inner product space, over \(R\) or \(C\)

DefinitionBernoulli law#

The Bernoulli distribution over an arbitrary measurable space X. Given x y : X and p : I (I is the unitInterval), it is the measure which gives mass p to {x} and 1 - p to {y}.

ProbabilityTheory.bernoulliMeasure.{u_1} {X : Type u_1} [MeasurableSpace X] (x y : X)
  (p : ↑unitInterval) : MeasureTheory.Measure X
Sources
MathlibProbabilityTheory.bernoulliMeasure
Uses 3 · Used by 1
Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Positive measure
Used byBinomial law

DefinitionBinomial law#

The binomial probability distribution with parameter p.

ProbabilityTheory.binomial (n : ℕ) (p : ↑unitInterval) : MeasureTheory.Measure ℕ
Sources
MathlibProbabilityTheory.binomial
Uses 8
Statement usesAlmost sure convergence · Bernoulli law · Carathéodory's extension theorem · Cardinal · Linear map · Measurable function · Probability measure · Product of finitely many measures

DefinitionGeometric law#

The geometric measure with success probability p as a measure over ℕ.

ProbabilityTheory.geometricMeasure (p : ↑unitInterval) : MeasureTheory.Measure ℕ
Sources
MathlibProbabilityTheory.geometricMeasure
Uses 4
Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Order · Positive measure

DefinitionPoisson law#

The poisson measure with rate r : ℝ≥0 as a measure over ℕ.

ProbabilityTheory.poissonMeasure (r : NNReal) : MeasureTheory.Measure ℕ
Sources
MathlibProbabilityTheory.poissonMeasure
Uses 4
Statement usesAssociative algebra over a commutative ring · Carathéodory's theorem (measure theory) · Exponential · Positive measure

DefinitionExponential law#

Measure defined by the exponential distribution

ProbabilityTheory.expMeasure (r : ℝ) : MeasureTheory.Measure ℝ
Sources
MathlibProbabilityTheory.expMeasure
Uses 4
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Exponential · Lebesgue measure (Measures and integral calculus)

DefinitionGaussian law#

A Gaussian distribution on ℝ with mean μ and variance v.

ProbabilityTheory.gaussianReal (μ : ℝ) (v : NNReal) : MeasureTheory.Measure ℝ
Sources
MathlibProbabilityTheory.gaussianReal
Uses 6 · Used by 2
Statement usesCarathéodory's theorem (measure theory) · Cos (extension of trigonometric functions to the complex plane) · Exponential · Integral of positive measurable functions · Lebesgue measure (Measures and integral calculus) · Linear map
Used byCentral limit theorem · Gaussian measures

ClassGaussian measures#

A measure is Gaussian if its map by every continuous linear form is a real Gaussian measure.

ProbabilityTheory.IsGaussian.{u_1} {E : Type u_1} [TopologicalSpace E] [AddCommMonoid E]
  [_root_.Module ℝ E] {mE : MeasurableSpace E} (μ : MeasureTheory.Measure E) : Prop
Sources
MathlibProbabilityTheory.IsGaussian
Uses 4 · Used by 2
Statement usesDual of a normed space · Gaussian law · Measurable function · Variance of a real-valued random variable
Used byGaussian processes · Fernique's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.