Probability and statistics

TheoremBayes' theorem #

Bayes' Theorem

ProbabilityTheory.cond_eq_inv_mul_cond_mul.{u_1} {Ω : Type u_1} {m : MeasurableSpace Ω}
  {s t : Set Ω} (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure μ] : μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t

Sources

MathlibProbabilityTheory.cond_eq_inv_mul_cond_mul

Uses 1

Statement usesConditional probability

TheoremContinuous mapping theorem #

Continuous mapping theorem: if X n tends to Z in distribution and g is continuous, then g ∘ X n tends to g ∘ Z in distribution.

MeasureTheory.TendstoInDistribution.continuous_comp.{u_1, u_2, u_3, u_5, u_6} {ι : Type u_1}
  {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ']
  {mE : MeasurableSpace E} {X : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [TopologicalSpace E]
  {F : Type u_6} [OpensMeasurableSpace E] [TopologicalSpace F] [MeasurableSpace F] [BorelSpace F]
  {g : E → F} (hg : Continuous g) (h : MeasureTheory.TendstoInDistribution X l Z μ μ') :
  MeasureTheory.TendstoInDistribution (fun n => g ∘ X n) l (g ∘ Z) μ μ'

Sources

MathlibMeasureTheory.TendstoInDistribution.continuous_comp

Uses 8 · Used by 2

Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Continuous function · Linear map · Measurable function · Probability measure

Used byCentral limit theorem · Slutsky's theorem

DefinitionIonescu-Tulcea theorem #

Ionescu-Tulcea Theorem : Given a family of kernels κ n taking variables in Iic n with value in X (n + 1), the kernel traj κ a takes a variable x depending on the variables i ≤ a and associates to it a kernel on trajectories depending on all variables, where the entries with index ≤ a are those of x, and then one follows iteratively the kernels κ a, then κ (a + 1), and so on.

The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of the Ionescu-Tulcea theorem.

ProbabilityTheory.Kernel.traj.{u_1} {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) :
  ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((n : ℕ) → X n)

Sources

MathlibProbabilityTheory.Kernel.traj

Uses 9

Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Carathéodory's extension theorem · Giry monad · Integral of positive measurable functions · Linear map · Measurable function · Probability measure · Product of sigma-algebras

TheoremLévy continuity theorem #

The Lévy convergence theorem: the weak convergence of probability measures is equivalent to the pointwise convergence of their characteristic functions.

MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {μ₀ : MeasureTheory.ProbabilityMeasure E}
  {μ : ℕ → MeasureTheory.ProbabilityMeasure E} :
  Filter.Tendsto μ Filter.atTop (nhds μ₀) ↔
    ∀ (t : E),
      Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop
        (nhds (MeasureTheory.charFun (↑μ₀) t))

Sources

MathlibMeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun

Uses 13 · Used by 1

Statement usesBorel sigma-algebra · Characteristic function · Finite-dimensionality · Probability measure

Proof usesChange of variable · Dominated convergence theorem · Field \(\C\) of complex numbers · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Limits of sequences · Lipschitz continuity · Pointwise convergence · Prokhorov's theorem · Squeeze theorem

Used byCentral limit theorem

Optional stopping theorem

TheoremPoisson limit theorem #

Poisson limit Theorem: If n * p n → r as n → ∞. Then (n.choose k) * (p n)^k * (1 - p n)^(n - k) → exp (-r) * r^k / k!.

ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop {p : ℕ → ℝ} {r : ℝ} (k : ℕ)
  (hr : Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r)) :
  Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k * (1 - p n) ^ (n - k)) Filter.atTop
    (nhds (Real.exp (-r) * r ^ k / ↑k.factorial))

Sources

MathlibProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop

Uses 12

Statement usesBornology · Exponential

Proof usesAssociative algebra over a commutative ring · Characteristic zero · Completeness · Field \(\Q\) of rational numbers · Normed vector space over a normed field · Ordered ring · The Binomial Theorem · The Triangle Inequality · Topological module · Topological ring

TheoremSlutsky's theorem #

Slutsky's theorem for a continuous function: if X n converges in distribution to Z, Y n converges in probability to a constant c, and g is a continuous function, then g (X n, Y n) converges in distribution to g (Z, c).

MeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const.{u_1, u_2, u_3,
    u_4, u_6, u_7}
  {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {m' : MeasurableSpace Ω'}
  {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ']
  {m'' : MeasurableSpace Ω''} {μ'' : MeasureTheory.Measure Ω''}
  [MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [SeminormedAddCommGroup E] [SecondCountableTopology E] [BorelSpace E] {E' : Type u_6}
  {F : Type u_7} {mE' : MeasurableSpace E'} [SeminormedAddCommGroup E'] [SecondCountableTopology E']
  [BorelSpace E'] [TopologicalSpace F] [MeasurableSpace F] [BorelSpace F] {g : E × E' → F}
  (hg : Continuous g) [l.IsCountablyGenerated] {X : ι → Ω'' → E} {Y : ι → Ω'' → E'} {c : E'}
  (hXZ : MeasureTheory.TendstoInDistribution X l Z (fun x => μ'') μ')
  (hY_tendsto : MeasureTheory.TendstoInMeasure μ'' Y l fun x => c)
  (hY : ∀ (i : ι), AEMeasurable (Y i) μ'') :
  MeasureTheory.TendstoInDistribution (fun n ω => g (X n ω, Y n ω)) l (fun ω => g (Z ω, c))
    (fun x => μ'') μ'

Sources

MathlibMeasureTheory.TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const

Uses 20

Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Bornology · Carathéodory's theorem (measure theory) · Continuous function · Convergence in probability · Linear map · Measurable function · Order · Probability measure

Proof usesCharacteristic zero · Completeness of R · Continuous mapping theorem · Convergence in distribution · Fatou's lemma · Inner product space, over \(R\) or \(C\) · Lipschitz continuity · Metric structure · Topological ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Probability and statistics

TheoremBayes' theorem#

Sources

TheoremContinuous mapping theorem#

Sources

DefinitionIonescu-Tulcea theorem#

Sources

TheoremLévy continuity theorem#

Sources

TheoremPoisson limit theorem#

Sources

TheoremSlutsky's theorem#

Sources

TheoremBayes' theorem #

TheoremContinuous mapping theorem #

DefinitionIonescu-Tulcea theorem #

TheoremLévy continuity theorem #

TheoremPoisson limit theorem #

TheoremSlutsky's theorem #