Distributions

Results named in Tau Ceti's TauCeti.Probability.Distributions modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremLebesgue decomposition#

A multivariate Gaussian mixture is the sum of its weighted components whose covariance is not positive definite, each singular with respect to Lebesgue measure by mutuallySingular_multivariateGaussian_volume, and of Lebesgue measure weighted by the mixture density.

TauCeti.Probability.multivariateGaussianMixtureMeasure_eq_add_withDensity.{u_1, u_2} {κ : Type u_1}
  {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ)
  (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) :
  TauCeti.Probability.multivariateGaussianMixtureMeasure p m S =
    ∑ k with ¬(S k).PosDef, ↑(p.weights k) • ProbabilityTheory.multivariateGaussian (m k) (S k) +
      MeasureTheory.volume.withDensity (TauCeti.Probability.multivariateGaussianMixturePDF p m S)
Lean

Formalized in Tau Ceti as TauCeti.Probability.multivariateGaussianMixtureMeasure_eq_add_withDensity.

Sources
LeanTauCeti.Probability.multivariateGaussianMixtureMeasure_eq_add_withDensity

TheoremThe Lévy–Khintchine formula for stable exponents#

For 0 < α < 2 and |β| ≤ 1, integrating the sine-compensated characteristic kernel against the stable Lévy measure gives the stable characteristic exponent in Nolan's S₀ parameterization.

TauCeti.Probability.integral_exp_sub_one_sub_sin_stableLevyMeasure {α β : ℝ} (hα : α ∈ Set.Ioo 0 2)
  (hβ : |β| ≤ 1) (t : ℝ) :
  ∫ (x : ℝ),
      Complex.exp (↑(t * x) * Complex.I) - 1 -
        ↑(t * Real.sin x) * Complex.I ∂TauCeti.Probability.stableLevyMeasure α β =
    TauCeti.Probability.stableCharacteristicExponent α β t
Lean

Formalized in Tau Ceti as TauCeti.Probability.integral_exp_sub_one_sub_sin_stableLevyMeasure.

Sources
LeanTauCeti.Probability.integral_exp_sub_one_sub_sin_stableLevyMeasure

TheoremThe Maurey–Pisier inequality#

For a centred Gaussian measure μ and a C¹ function f, ∫∫ exp (t (f y - f x)) dμ(x) dμ(y) ≤ ∫ exp (π² t² / 8 · Var[f' x; μ]) dμ(x).

ProbabilityTheory.IsGaussian.lintegral_exp_mul_sub_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [CompleteSpace E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] {f : E → ℝ}
  (hμ : ∫ (x : E), id x ∂μ = 0) (hf : ContDiff ℝ 1 f) (t : ℝ) :
  ∫⁻ (p : E × E), ENNReal.ofReal (Real.exp (t * (f p.2 - f p.1))) ∂μ.prod μ ≤
    ∫⁻ (x : E),
      ENNReal.ofReal
        (Real.exp (Real.pi ^ 2 * t ^ 2 / 8 * ProbabilityTheory.variance (⇑(fderiv ℝ f x)) μ)) ∂μ
Lean

Formalized in Tau Ceti as ProbabilityTheory.IsGaussian.lintegral_exp_mul_sub_le.

Sources
LeanProbabilityTheory.IsGaussian.lintegral_exp_mul_sub_le

TheoremParseval's identity for the Gaussian Hermite basis#

The squared norms of the Gaussian Hermite coefficients of f sum to ‖f‖².

TauCeti.tsum_norm_sq_integral_hermite_mul_gaussianReal.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 (ProbabilityTheory.gaussianReal 0 1))) :
  ∑' (n : ℕ),
      ‖∫ (x : ℝ),
            (algebraMap ℝ 𝕜) ((Polynomial.aeval x) (Polynomial.hermite n) / √↑n.factorial) *
              ↑↑f x ∂ProbabilityTheory.gaussianReal 0 1‖ ^
        2 =
    ‖f‖ ^ 2
Lean

Formalized in Tau Ceti as TauCeti.tsum_norm_sq_integral_hermite_mul_gaussianReal.

Other forms

Parseval's identity for the multivariate Gaussian Hermite basis (polarized form). Formalized in Tau Ceti as TauCeti.tsum_inner_mul_inner_L2piMul_gaussianHermiteHilbertBasis.

TauCeti.tsum_inner_mul_inner_L2piMul_gaussianHermiteHilbertBasis.{u_1, u_2} {𝕜 : Type u_1}
  [RCLike 𝕜] {ι : Type u_2} [Fintype ι]
  (f g :
    ↥(MeasureTheory.Lp 𝕜 2
        (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1))) :
  ∑' (a : ι → ℕ),
      inner 𝕜 f (TauCeti.L2piMul fun i => (TauCeti.gaussianHermiteHilbertBasis 𝕜) (a i)) *
        inner 𝕜 (TauCeti.L2piMul fun i => (TauCeti.gaussianHermiteHilbertBasis 𝕜) (a i)) g =
    inner 𝕜 f g

Parseval's identity for the multivariate Gaussian Hermite basis. Formalized in Tau Ceti as TauCeti.tsum_norm_sq_integral_prod_hermite_mul_pi_gaussianReal.

TauCeti.tsum_norm_sq_integral_prod_hermite_mul_pi_gaussianReal.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜]
  {ι : Type u_2} [Fintype ι]
  (f :
    ↥(MeasureTheory.Lp 𝕜 2
        (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1))) :
  ∑' (a : ι → ℕ),
      ‖∫ (x : ι → ℝ),
            (∏ i,
                (algebraMap ℝ 𝕜)
                  ((Polynomial.aeval (x i)) (Polynomial.hermite (a i)) / √↑(a i).factorial)) *
              ↑↑f x ∂MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1‖ ^
        2 =
    ‖f‖ ^ 2
Sources
LeanTauCeti.tsum_norm_sq_integral_hermite_mul_gaussianReal · TauCeti.tsum_inner_mul_inner_L2piMul_gaussianHermiteHilbertBasis · TauCeti.tsum_norm_sq_integral_prod_hermite_mul_pi_gaussianReal
Uses 4
Statement usesThe weighted-measure basis
Proof usesThe Fintype-indexed product Hilbert basis · Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis) · Parseval's identity for a functional

TheoremRademacher convexity inequality#

Every summand's norm is bounded by the expected norm of the signed sum. Pairwise independence of the Rademacher signs suffices.

Finset.norm_le_integral_norm_sum_smul_rademacher.{u_1, u_2, u_3} {Ω : Type u_1} {ι : Type u_2}
  {E : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {ε : ι → Ω → ℝ} (s : Finset ι) (v : ι → E)
  (hε : ∀ i ∈ s, ProbabilityTheory.HasLaw (ε i) TauCeti.Probability.rademacherMeasure P)
  (hind : (↑s).Pairwise fun i j => ProbabilityTheory.IndepFun (ε i) (ε j) P) {j : ι} (hj : j ∈ s) :
  ‖v j‖ ≤ ∫ (ω : Ω), ‖∑ i ∈ s, ε i ω • v i‖ ∂P
Lean

Formalized in Tau Ceti as Finset.norm_le_integral_norm_sum_smul_rademacher.

Sources
LeanFinset.norm_le_integral_norm_sum_smul_rademacher

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.