Convergence of a sequence of random variables

DefinitionConvergence in probability#

A sequence of functions f is said to converge in measure to some function g if for all ε > 0, the measure of the set {x | ε ≤ dist (f i x) (g x)} tends to 0 as i converges along some given filter l.

MeasureTheory.TendstoInMeasure.{u_1, u_2, u_4} {α : Type u_1} {ι : Type u_2} {E : Type u_4}
  [EDist E] {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : ι → α → E) (l : Filter ι)
  (g : α → E) : Prop
Sources
MathlibMeasureTheory.TendstoInMeasure
Uses 1 · Used by 2
Statement usesPositive measure
Used byVitali convergence theorem · Slutsky's theorem

DefinitionAlmost sure convergence#

The “almost everywhere” filter of co-null sets.

MeasureTheory.ae.{u_1, u_3} {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal]
  [MeasureTheory.OuterMeasureClass F α] (μ : F) : Filter α
Sources
MathlibMeasureTheory.ae
Uses 2 · Used by 25
Statement usesInfinite sum · Real number
Used byMinkowski’s Fundamental Theorem · Fatou's lemma · \(L^p\) space · Monotone convergence theorem (Measures and integral calculus) · Uniform integrability · Vector-valued integrable function (Bochner integral) · Markov inequality · Independent events · Independent sigma-algebras · Binomial law · Independence of random variables · Probability density function · Lebesgue differentiation theorem · Rademacher's theorem · Bounded convergence theorem · Egorov's theorem · Steinhaus theorem · Vitali convergence theorem · Poincaré recurrence theorem · Lebesgue's density theorem · Dirichlet's approximation theorem · Continuous mapping theorem · Ionescu-Tulcea theorem · Slutsky's theorem · Hölder's inequality

TheoremConvergence in distribution#

The characterization of weak convergence of probability measures by the usual (defining) condition that the integrals of every continuous bounded function converge to the integral of the function against the limit measure.

MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.{u_1, u_2} {Ω : Type u_1}
  [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {γ : Type u_2} {F : Filter γ}
  {μs : γ → MeasureTheory.ProbabilityMeasure Ω} {μ : MeasureTheory.ProbabilityMeasure Ω} :
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω ℝ),
      Filter.Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (nhds (∫ (ω : Ω), f ω ∂↑μ))
Sources
MathlibMeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
Uses 2 · Used by 1
Statement usesBochner integral · Probability measure
Used bySlutsky's theorem

TheoremMarkov inequality#

Markov's inequality also known as Chebyshev's first inequality. For a version assuming AEMeasurable, see mul_meas_ge_le_lintegral₀.

MeasureTheory.mul_meas_ge_le_lintegral.{u_1} {α : Type u_1} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (ε : ENNReal) :
  ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
Sources
MathlibMeasureTheory.mul_meas_ge_le_lintegral
Uses 9
Statement usesIntegral of positive measurable functions · Measurable function
Proof usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Continuous function · Linear map · Order topology

TheoremChebyshev inequality#

Chebyshev's inequality: one can control the deviation probability of a real random variable from its expectation in terms of the variance.

ProbabilityTheory.meas_ge_le_variance_div_sq.{u_1} {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ}
  (hX : MeasureTheory.MemLp X 2 μ) {c : ℝ} (hc : 0 < c) :
  μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (ProbabilityTheory.variance X μ / c ^ 2)
Sources
MathlibProbabilityTheory.meas_ge_le_variance_div_sq
Uses 3 · Used by 1
Statement usesVariance of a real-valued random variable
Proof usesCharacteristic zero · Field \(\R\) of real numbers
Used byStrong law of large numbers

TheoremStrong law of large numbers#

Strong law of large numbers, almost sure version: if X n is a sequence of independent identically distributed integrable random variables taking values in a Banach space, then n⁻¹ • ∑ i ∈ range n, X i converges almost surely to 𝔼[X 0]. We give here the strong version, due to Etemadi, that only requires pairwise independence.

ProbabilityTheory.strong_law_ae.{u_1, u_2} {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (X : ℕ → Ω → E)
  (hint : MeasureTheory.Integrable (X 0) μ)
  (hindep : Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X))
  (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) :
  ∀ᵐ (ω : Ω) ∂μ,
    Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) Filter.atTop
      (nhds (∫ (x : Ω), X 0 x ∂μ))
Sources
MathlibProbabilityTheory.strong_law_ae
Uses 19
Statement usesAssociative algebra over a commutative ring · Bochner integral · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Giry monad · Measurable function
Proof usesApproximation by step functions · Borel-Cantelli lemma (easy direction) · Chebyshev inequality · Compactness in terms of filters · Completeness of R · Hausdorff space · Lebesgue measure (Measure theory) · Metric structure · Pointwise convergence · Probability measure · The Triangle Inequality · Topological module · Topological ring

TheoremCentral limit theorem#

Central Limit Theorem: Given a sequence of random variables X : ℕ → Ω → ℝ that are independent, identically distributed with mean μ and variance v, and a random variable Y : Ω' → ℝ following gaussianReal 0 v, the sequence n ↦ (√n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ) converges to Y in distribution.

ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub.{u_1, u_2} {Ω : Type u_1}
  {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω}
  {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ}
  [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure P']
  (hY :
    ProbabilityTheory.HasLaw Y
      (ProbabilityTheory.gaussianReal 0 (ProbabilityTheory.variance (X 0) P).toNNReal) P')
  (hX : MeasureTheory.MemLp (X 0) 2 P) (hindep : ProbabilityTheory.iIndepFun X P)
  (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) :
  MeasureTheory.TendstoInDistribution
    (fun n ω => (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) Filter.atTop Y
    (fun x => P) P'
Sources
MathlibProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub
Uses 7
Statement usesGaussian law · Independence of random variables · Probability measure · Variance of a real-valued random variable
Proof usesCharacteristic p · Continuous mapping theorem · Lévy continuity theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.