The cumulative distribution function of a beta law

This file computes ProbabilityTheory.cdf (betaMeasure α β) in closed form: for positive shape parameters it is the regularized incomplete beta function TauCeti.regularizedIncompleteBeta, I_x(α, β).

This is the beta entry of the closed-form cdf target of TauCetiRoadmap/StandardDistributions/README.md, Layer 2.

The identity holds for every real x, with no constraint to the unit interval: outside [0, 1] both sides are constant, because TauCeti.regularizedIncompleteBeta clamps its argument there. That agreement at the clamping convention is the reason the roadmap prescribes the totalization it does.

The proof splits Set.Iic x at the two ends of the support. Below the origin the density vanishes, so the cdf is 0; on [0, 1] the cdf integral is exactly the normalized beta integral defining I_x(α, β); and above 1 the extra piece contributes nothing, so the value is Euler's integral divided by itself, namely 1.

Main results

• TauCeti.Probability.cdf_betaMeasure_eq — the closed-form cdf I_x(α, β);
• TauCeti.Probability.cdf_betaMeasure_one_right — the power-function cdf x ^ α when β = 1;
• TauCeti.Probability.measureReal_Iic_betaMeasure — the same in measure form;
• TauCeti.Probability.measureReal_Ioc_betaMeasure — the mass of a bounded interval, as a difference of two values of I_·(α, β);
• TauCeti.Probability.measureReal_Ioi_betaMeasure — the upper tail 1 - I_x(α, β);
• TauCeti.Probability.continuous_cdf_betaMeasure — the cdf is continuous, so a beta law has no atoms;
• TauCeti.Probability.measureReal_le_of_hasLaw_betaMeasure — the random-variable corollary.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 2, the "Closed-form cdfs and tails" target.
• Formal template: TauCeti/Probability/Distributions/Gamma/Cdf.lean.
• NIST Digital Library of Mathematical Functions, §8.17.

The cdf as an integral of the density

The three ranges of the support

The closed form

@[simp]

theorem TauCeti.Probability.cdf_betaMeasure_eq {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.betaMeasure α β)) x = regularizedIncompleteBeta α β x

The cumulative distribution function of the beta law with positive shape parameters α and β is the regularized incomplete beta function, I_x(α, β).

No constraint on x is needed: outside [0, 1] both sides are constant, which is exactly the clamping convention built into TauCeti.regularizedIncompleteBeta.

theorem TauCeti.Probability.cdf_betaMeasure_one_right {α x : ℝ} (hα : 0 < α) (hx : x ∈ Set.Icc 0 1) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.betaMeasure α 1)) x = x ^ α

With second shape parameter one the beta law is the power-function law: on [0, 1] its cumulative distribution function is x ^ α.

Consequences

@[simp]

theorem TauCeti.Probability.measureReal_Iic_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (x : ℝ) : (ProbabilityTheory.betaMeasure α β).real (Set.Iic x) = regularizedIncompleteBeta α β x

The mass a beta law assigns to a lower half-line, in measure form.

@[simp]

theorem TauCeti.Probability.measureReal_Ioc_betaMeasure {α β x : ℝ} (hα : 0 < α) (hβ : 0 < β) {y : ℝ} (hyx : y ≤ x) : (ProbabilityTheory.betaMeasure α β).real (Set.Ioc y x) = regularizedIncompleteBeta α β x - regularizedIncompleteBeta α β y

The mass a beta law assigns to a bounded interval is the increment of I_·(α, β).

@[simp]

theorem TauCeti.Probability.measureReal_Ioi_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) (x : ℝ) : (ProbabilityTheory.betaMeasure α β).real (Set.Ioi x) = 1 - regularizedIncompleteBeta α β x

The upper tail of a beta law is 1 - I_x(α, β).

theorem TauCeti.Probability.continuous_cdf_betaMeasure {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) : Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.betaMeasure α β))

The cumulative distribution function of a beta law is continuous: I_·(α, β) is continuous even at the two endpoints of the support, where for α < 1 or β < 1 the beta integrand blows up.

theorem TauCeti.Probability.measureReal_le_of_hasLaw_betaMeasure {α β : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hα : 0 < α) (hβ : 0 < β) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.betaMeasure α β) P) (x : ℝ) : P.real {ω : Ω | X ω ≤ x} = regularizedIncompleteBeta α β x

A random variable with a beta law has the regularized incomplete beta function as its cumulative distribution function.