Standard probability distributions and their elementary theory

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe Bartlett decomposition of the standard Wishart law#

Lift TauCeti.Probability.nonsingularWishartMeasure n 1 to the positive-definite cone, where Cholesky factorization is defined, and read the on-or-below-diagonal entries of the factor: the resulting law is the product of the Bartlett coordinate laws. Cholesky factorization inverts the Gram map of TauCeti.Probability.map_lowerTriangleGram_pi_bartlettCoordinateMeasure, and the product law lives on the positive-diagonal region where that inversion is valid.

TauCeti.Probability.map_choleskyLowerCoordinates_comap_nonsingularWishartMeasure {p : ℕ} {n : ℝ}
  (hn : ↑p - 1 < n) :
  MeasureTheory.Measure.map (TauCeti.choleskyLowerCoordinates p)
      (MeasureTheory.Measure.comap Subtype.val
        (TauCeti.Probability.nonsingularWishartMeasure n 1)) =
    MeasureTheory.Measure.pi (TauCeti.Probability.bartlettCoordinateMeasure n)
Lean

Formalized in Tau Ceti as TauCeti.Probability.map_choleskyLowerCoordinates_comap_nonsingularWishartMeasure.

Other forms

The Bartlett decomposition. Formalized in Tau Ceti as TauCeti.Probability.bartlett_nonsingularWishartMeasure.

TauCeti.Probability.bartlett_nonsingularWishartMeasure.{u_1} {p : ℕ} {n : ℝ} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (hn : ↑p - 1 < n)
  {A : Ω → TauCeti.PosDefMatrix p}
  (hA :
    ProbabilityTheory.HasLaw A
      (MeasureTheory.Measure.comap Subtype.val (TauCeti.Probability.nonsingularWishartMeasure n 1))
      P) :
  ProbabilityTheory.iIndepFun (fun ij ω => ↑(TauCeti.cholesky (A ω)) (↑ij).1 (↑ij).2) P ∧
    (∀ (i : Fin p),
        ProbabilityTheory.HasLaw (fun ω => ↑(TauCeti.cholesky (A ω)) i i ^ 2)
          (TauCeti.Probability.chiSquaredMeasure (n - ↑↑i)) P) ∧
      ∀ (i j : Fin p),
        j < i →
          ProbabilityTheory.HasLaw (fun ω => ↑(TauCeti.cholesky (A ω)) i j)
            (ProbabilityTheory.gaussianReal 0 1) P
Sources
LeanTauCeti.Probability.map_choleskyLowerCoordinates_comap_nonsingularWishartMeasure · TauCeti.Probability.bartlett_nonsingularWishartMeasure

TheoremThe diagonal entries of an inverse-Wishart matrix are inverse gamma#

For a positive-definite scale S, the entry (i, i) of an inverse-Wishart matrix of degree n has the inverse-gamma law of shape (n - p + 1) / 2 and scale S i i / 2. For degrees at most p - 1 both sides are the zero measure.

TauCeti.Probability.map_coe_apply_inverseWishartMeasure {p : ℕ} {n : ℝ}
  {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.PosDef) (i : Fin p) :
  MeasureTheory.Measure.map (fun B => ↑B i i) (TauCeti.Probability.inverseWishartMeasure n S) =
    TauCeti.Probability.inverseGammaMeasure ((n - ↑p + 1) / 2) (S i i / 2)
Lean

Formalized in Tau Ceti as TauCeti.Probability.map_coe_apply_inverseWishartMeasure.

Sources
LeanTauCeti.Probability.map_coe_apply_inverseWishartMeasure

TheoremOrder statistics of uniform samples are beta distributed#

The k-th order statistic (counted from 0) of n independent uniform variables on the unit interval has the beta law with parameters k + 1 and n - k.

TauCeti.Probability.map_orderStatistic_pi_uniformMeasure {n : ℕ} (k : Fin n) :
  MeasureTheory.Measure.map (TauCeti.orderStatistic k)
      (MeasureTheory.Measure.pi fun x => TauCeti.Probability.uniformMeasure 0 1) =
    ProbabilityTheory.betaMeasure (↑↑k + 1) (↑n - ↑↑k)
Lean

Formalized in Tau Ceti as TauCeti.Probability.map_orderStatistic_pi_uniformMeasure.

Sources
LeanTauCeti.Probability.map_orderStatistic_pi_uniformMeasure

TheoremTauCeti.Probability.map_sum_sq_pi_gaussianReal_noncentral#

The sum of squares of independent unit-variance Gaussian coordinates has noncentral chi-squared law, including the empty family.

TauCeti.Probability.map_sum_sq_pi_gaussianReal_noncentral.{u_1} {ι : Type u_1} [Fintype ι]
  (m : ι → ℝ) :
  MeasureTheory.Measure.map (fun x => ∑ i, x i ^ 2)
      (MeasureTheory.Measure.pi fun i => ProbabilityTheory.gaussianReal (m i) 1) =
    TauCeti.Probability.noncentralChiSquaredMeasure (↑(Fintype.card ι)) (∑ i, ‖m i‖₊ ^ 2)
Lean

Formalized in Tau Ceti as TauCeti.Probability.map_sum_sq_pi_gaussianReal_noncentral.

Sources
LeanTauCeti.Probability.map_sum_sq_pi_gaussianReal_noncentral

DefinitionTauCeti.Probability.noncentralFPDFReal#

The noncentral F density as a Poisson series of scaled central F densities. Invalid degrees give zero.

TauCeti.Probability.noncentralFPDFReal (m n : ℝ) (l : NNReal) (x : ℝ) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.Probability.noncentralFPDFReal.

Sources
LeanTauCeti.Probability.noncentralFPDFReal

TheoremMeasureTheory.ProbabilityMeasure.tendsto_haarAddCircle_iff#

Circle probability measures tend weakly to Haar probability exactly when every nonzero integer Fourier moment tends to zero.

MeasureTheory.ProbabilityMeasure.tendsto_haarAddCircle_iff.{u_1} {T : ℝ} [Fact (0 < T)]
  {ι : Type u_1} {L : Filter ι} {μs : ι → MeasureTheory.ProbabilityMeasure (AddCircle T)} :
  Filter.Tendsto μs L (nhds AddCircle.haarAddCircle.toProbabilityMeasure) ↔
    ∀ (n : ℤ),
      n ≠ 0 → Filter.Tendsto (fun i => ∫ (x : AddCircle T), (fourier n) x ∂↑(μs i)) L (nhds 0)
Lean

Formalized in Tau Ceti as MeasureTheory.ProbabilityMeasure.tendsto_haarAddCircle_iff.

Sources
LeanMeasureTheory.ProbabilityMeasure.tendsto_haarAddCircle_iff

TheoremThe multivariate Gamma integral#

For ((p : ℝ) - 1) / 2 < a, the integral of (det A) ^ (a - (p + 1) / 2) * exp (-trace A) over the cone of positive-definite symmetric p × p matrices, against TauCeti.symmetricLebesgue p, is Γ_p(a).

TauCeti.integral_posDef_multivariateGamma {p : ℕ} {a : ℝ} (ha : (↑p - 1) / 2 < a) :
  ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A | (↑A).PosDef},
      (↑A).det ^ (a - (↑p + 1) / 2) * Real.exp (-(↑A).trace) ∂TauCeti.symmetricLebesgue p =
    TauCeti.multivariateGamma p a
Lean

Formalized in Tau Ceti as TauCeti.integral_posDef_multivariateGamma.

Sources
LeanTauCeti.integral_posDef_multivariateGamma

DefinitionTauCeti.inverseRegularizedGamma#

The inverse P⁻¹(s, u) of the regularized lower incomplete gamma function in its argument.

For positive s this is the quantile of the Gamma law with shape s and rate 1. For nonpositive s it is 0; the quantile itself supplies the value 0 outside 0 < u < 1.

TauCeti.inverseRegularizedGamma (s u : ℝ) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.inverseRegularizedGamma.

Sources
LeanTauCeti.inverseRegularizedGamma

DefinitionTauCeti.Probability.vonMisesFisherNaturalMeasure#

The von Mises–Fisher law with natural parameter η, relative to uniform sphere probability. In dimension zero the sphere and this measure are empty.

TauCeti.Probability.vonMisesFisherNaturalMeasure.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (η : E) :
  MeasureTheory.Measure ↑(Metric.sphere 0 1)
Lean

Formalized in Tau Ceti as TauCeti.Probability.vonMisesFisherNaturalMeasure.

Sources
LeanTauCeti.Probability.vonMisesFisherNaturalMeasure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.