Elementary theory of the beta distribution

This file completes the elementary moment theory of Mathlib's beta distribution. For positive shape parameters it computes every natural raw moment, and obtains the mean and variance as the first two cases. It also records that the beta law is carried by [0, 1], so every exponential moment exists.

Main results

• TauCeti.Probability.betaPDFReal_nonneg — nonnegativity of the density;
• TauCeti.Probability.integrable_betaMeasure_iff and TauCeti.Probability.integral_betaMeasure_eq — integrability and integration against the beta law, transferred to the real density;
• TauCeti.Probability.betaMeasure_eq_withDensity_restrict_Ioo — the law is its density against Lebesgue measure on the open unit interval;
• TauCeti.Probability.integral_pow_betaMeasure — the natural raw moments as a quotient of Gamma values;
• TauCeti.Probability.integral_id_betaMeasure — the mean is α / (α + β);
• TauCeti.Probability.variance_id_betaMeasure — the variance is α * β / ((α + β) ^ 2 * (α + β + 1));
• TauCeti.Probability.integrableExpSet_id_betaMeasure — every exponential moment exists.

The moment calculation rewrites the density integral as Euler's beta integral — the real-valued TauCeti.integral_rpow_mul_one_sub_rpow, proved in TauCeti/Analysis/SpecialFunctions/Beta.lean — and then uses the Gamma quotient.

References

• Tau Ceti roadmap, StandardDistributions, Layer 1, "Beta".
• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley, 1995.

theorem TauCeti.Probability.betaPDFReal_nonneg {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (x : ℝ) : 0 ≤ ProbabilityTheory.betaPDFReal α β x

For positive shape parameters the beta density is nonnegative: it vanishes off the open unit interval, and on it the normalizing constant ProbabilityTheory.beta α β is positive.

theorem TauCeti.Probability.betaMeasure_eq_withDensity_ofReal (α β : ℝ) : ProbabilityTheory.betaMeasure α β = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.betaPDFReal α β x)

The beta law presented by its real-valued density.

theorem TauCeti.Probability.integrable_betaMeasure_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) {g : ℝ → E} : MeasureTheory.Integrable g (ProbabilityTheory.betaMeasure α β) ↔ MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.betaPDFReal α β x • g x) MeasureTheory.volume

Integrability transfer. A function is integrable against a beta law with positive shape parameters exactly when its density-weighted version is Lebesgue integrable.

theorem TauCeti.Probability.integral_betaMeasure_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (g : ℝ → E) : ∫ (x : ℝ), g x ∂ProbabilityTheory.betaMeasure α β = ∫ (x : ℝ), ProbabilityTheory.betaPDFReal α β x • g x

Integral transfer. An integral against a beta law with positive shape parameters is the density-weighted Lebesgue integral.

theorem TauCeti.Probability.ae_mem_Ioo_betaMeasure (α β : ℝ) : ∀ᵐ (x : ℝ) ∂ProbabilityTheory.betaMeasure α β, x ∈ Set.Ioo 0 1

A beta measure lies almost everywhere in the open unit interval, for all parameter values.

theorem TauCeti.Probability.betaMeasure_eq_withDensity_restrict_Ioo (α β : ℝ) : ProbabilityTheory.betaMeasure α β = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).withDensity (ProbabilityTheory.betaPDF α β)

The beta law is its density against Lebesgue measure on the open unit interval: the density vanishes off the closed interval, and the two endpoints are null.

theorem TauCeti.Probability.ae_mem_Icc_betaMeasure (α β : ℝ) : ∀ᵐ (x : ℝ) ∂ProbabilityTheory.betaMeasure α β, x ∈ Set.Icc 0 1

The beta distribution is carried by the unit interval.

@[simp]

theorem TauCeti.Probability.integral_pow_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (n : ℕ) : ∫ (x : ℝ), x ^ n ∂ProbabilityTheory.betaMeasure α β = Real.Gamma (α + ↑n) * Real.Gamma (α + β) / (Real.Gamma α * Real.Gamma (α + β + ↑n))

The nth raw moment of a beta distribution with positive shape parameters.

@[simp]

theorem TauCeti.Probability.integral_id_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : ∫ (x : ℝ), x ∂ProbabilityTheory.betaMeasure α β = α / (α + β)

The mean of a beta distribution with positive shape parameters.

@[simp]

theorem TauCeti.Probability.variance_id_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : ProbabilityTheory.variance id (ProbabilityTheory.betaMeasure α β) = α * β / ((α + β) ^ 2 * (α + β + 1))

The variance of a beta distribution with positive shape parameters.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : ProbabilityTheory.integrableExpSet id (ProbabilityTheory.betaMeasure α β) = Set.univ

Every exponential moment of a beta distribution with positive shape parameters exists.