The regularized incomplete beta function

For positive shape parameters a and b the regularized incomplete beta function is I_x(a, b) = (∫ t in 0..x, t ^ (a - 1) * (1 - t) ^ (b - 1)) / Β(a, b), where Β is Euler's beta function ProbabilityTheory.beta. It is the cumulative distribution function of the beta law, and it also expresses the cumulative distribution functions of Student's t, Fisher's F and the negative binomial law, together with the binomial tail.

TauCeti.regularizedIncompleteBeta clamps its argument to [0, 1], so it is defined — and equal to the cdf of the beta law — on all of ℝ. Outside the positive parameter range it is zero, with one deliberate exception: regularizedIncompleteBeta 0 b x = 1 for 0 < b and 0 ≤ x. This records the cdf of the weak limit betaMeasure a b → Measure.dirac 0 as a → 0⁺, and it is what makes the binomial-tail formula (binomial n p).real {k | m ≤ k} = I_p(m, n - m + 1) hold at m = 0 without a separate case.

The real-variable theory of Euler's beta integral that the construction rests on lives in TauCeti/Analysis/SpecialFunctions/Beta.lean.

Main results

• TauCeti.regularizedIncompleteBeta — the definition;
• TauCeti.regularizedIncompleteBeta_def_of_pos and TauCeti.regularizedIncompleteBeta_def_of_mem_Icc — the defining normalized integral, with the clamp displayed and with the clamp already discharged on [0, 1];
• TauCeti.regularizedIncompleteBeta_zero_left — the value 1 at the boundary a = 0;
• TauCeti.regularizedIncompleteBeta_eq_zero_of_nonpos, TauCeti.regularizedIncompleteBeta_eq_zero_of_neg and TauCeti.regularizedIncompleteBeta_eq_one_of_one_le — the values 0 and 1 off (0, 1);
• TauCeti.regularizedIncompleteBeta_eq_zero_of_neg_left and TauCeti.regularizedIncompleteBeta_eq_zero_of_nonpos_right — the default value 0 outside the parameter range;
• TauCeti.regularizedIncompleteBeta_monotone — monotonicity, for every choice of parameters;
• TauCeti.regularizedIncompleteBeta_nonneg and TauCeti.regularizedIncompleteBeta_le_one — the range [0, 1], for every choice of parameters;
• TauCeti.continuous_regularizedIncompleteBeta — continuity on all of ℝ;
• TauCeti.hasDerivAt_regularizedIncompleteBeta — the derivative on (0, 1);
• TauCeti.integral_Ioi_rpow_one_add_rpow_eq_interval_tail and TauCeti.integral_Ioi_rpow_one_add_rpow_tail_eq — the second-beta-integral upper tail, rewritten through the incomplete beta function;
• TauCeti.regularizedIncompleteBeta_symm — the reflection formula I_x(a, b) = 1 - I_{1-x}(b, a);
• TauCeti.regularizedIncompleteBeta_one_right and TauCeti.regularizedIncompleteBeta_one_left — the elementary values x ^ a and 1 - (1 - x) ^ b at a unit parameter;
• TauCeti.regularizedIncompleteBeta_add_one_left and TauCeti.regularizedIncompleteBeta_add_one_right — the unit-step recurrences I_x(a + 1, b) = I_x(a, b) - x ^ a * (1 - x) ^ b / (a * Β(a, b)) and I_x(a, b + 1) = I_x(a, b) + x ^ a * (1 - x) ^ b / (b * Β(a, b)), for 0 ≤ x ≤ 1;
• TauCeti.regularizedIncompleteBeta_add_one_right_sub_add_one_left — the step along the antidiagonal a + b = const, whose increment is a generalized binomial coefficient.

References

• Tau Ceti roadmap, StandardDistributions, Layer 2, "Regularized incomplete beta".
• NIST Digital Library of Mathematical Functions, §8.17; the recurrence is 8.17.20.

noncomputable def TauCeti.regularizedIncompleteBeta (a b x : ℝ) : ℝ

The regularized incomplete beta function I_x(a, b), extended to all real arguments by clamping x to [0, 1]. It is zero outside the positive parameter range, except that regularizedIncompleteBeta 0 b x = 1 for 0 < b and 0 ≤ x; that convention records the cdf of the weak limit of betaMeasure a b as a → 0⁺.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.regularizedIncompleteBeta_def_of_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (x : ℝ) : regularizedIncompleteBeta a b x = (∫ (t : ℝ) in 0..min 1 (max x 0), t ^ (a - 1) * (1 - t) ^ (b - 1)) / ProbabilityTheory.beta a b

On the positive parameter range the regularized incomplete beta function is the normalized integral of the beta integrand up to the clamped argument.

theorem TauCeti.regularizedIncompleteBeta_def_of_mem_Icc {a b x : ℝ} (ha : 0 < a) (hb : 0 < b) (hx : x ∈ Set.Icc 0 1) : regularizedIncompleteBeta a b x = (∫ (t : ℝ) in 0..x, t ^ (a - 1) * (1 - t) ^ (b - 1)) / ProbabilityTheory.beta a b

On the support [0, 1] the clamp is invisible: the regularized incomplete beta function is the normalized integral of the beta integrand up to x itself. This is the form in which the cumulative distribution functions built from TauCeti.regularizedIncompleteBeta are used.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_zero_left {b x : ℝ} (hb : 0 < b) (hx : 0 ≤ x) : regularizedIncompleteBeta 0 b x = 1

The boundary convention at a = 0: the regularized incomplete beta function is the cdf of Measure.dirac 0, the weak limit of betaMeasure a b as a → 0⁺.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_eq_zero_of_neg_left {a : ℝ} (ha : a < 0) (b x : ℝ) : regularizedIncompleteBeta a b x = 0

The regularized incomplete beta function vanishes when its first parameter is negative: no beta law is attached to such parameters, and the definition takes its default value there.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_eq_zero_of_nonpos_right {b : ℝ} (hb : b ≤ 0) (a x : ℝ) : regularizedIncompleteBeta a b x = 0

The regularized incomplete beta function vanishes when its second parameter is nonpositive. Unlike the first parameter, the second admits no exceptional value at 0: the weak limit of betaMeasure a b as b → 0⁺ is Measure.dirac 1, whose cdf is not the constant 1.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_eq_zero_of_neg {x : ℝ} (a b : ℝ) (hx : x < 0) : regularizedIncompleteBeta a b x = 0

The regularized incomplete beta function vanishes strictly below the support of the beta law, for every choice of parameters: the exceptional value 1 at a = 0 is taken from 0 onwards.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_eq_zero_of_nonpos {a x : ℝ} (ha : a ≠ 0) (b : ℝ) (hx : x ≤ 0) : regularizedIncompleteBeta a b x = 0

The regularized incomplete beta function vanishes below the support of the beta law. The hypothesis a ≠ 0 is needed only at x = 0, where the boundary convention gives the value 1; TauCeti.regularizedIncompleteBeta_eq_zero_of_neg is the unconditional statement strictly below 0.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_eq_one_of_one_le {a b x : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hx : 1 ≤ x) : regularizedIncompleteBeta a b x = 1

The regularized incomplete beta function is 1 above the support of the beta law, including at the boundary parameter a = 0.

theorem TauCeti.regularizedIncompleteBeta_monotone (a b : ℝ) : Monotone (regularizedIncompleteBeta a b)

The regularized incomplete beta function is monotone, for every choice of parameters: it is a normalized integral of a nonnegative density when 0 < a and 0 < b, the unit step at 0 when a = 0 < b, and the zero function for all remaining parameters.

theorem TauCeti.regularizedIncompleteBeta_nonneg (a b x : ℝ) : 0 ≤ regularizedIncompleteBeta a b x

The regularized incomplete beta function is nonnegative.

theorem TauCeti.regularizedIncompleteBeta_le_one (a b x : ℝ) : regularizedIncompleteBeta a b x ≤ 1

The regularized incomplete beta function is at most 1.

theorem TauCeti.continuous_regularizedIncompleteBeta {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Continuous (regularizedIncompleteBeta a b)

The regularized incomplete beta function is continuous on all of ℝ, including at the two endpoints of the support, where the integrand may blow up.

theorem TauCeti.hasDerivAt_regularizedIncompleteBeta {a b x : ℝ} (ha : 0 < a) (hb : 0 < b) (hx0 : 0 < x) (hx1 : x < 1) : HasDerivAt (regularizedIncompleteBeta a b) (x ^ (a - 1) * (1 - x) ^ (b - 1) / ProbabilityTheory.beta a b) x

The derivative of the regularized incomplete beta function on the open unit interval is the normalized beta density. No differentiability is claimed at the endpoints: for a < 1 or b < 1 the density is unbounded there.

Tails

theorem TauCeti.integral_Ioi_rpow_one_add_rpow_eq_interval_tail {a b u0 : ℝ} (hu00 : 0 ≤ u0) (hu01 : u0 < 1) : ∫ (w : ℝ) in Set.Ioi (u0 / (1 - u0)), w ^ (a - 1) * (1 + w) ^ (-(a + b)) = ∫ (u : ℝ) in Set.Ioo u0 1, u ^ (a - 1) * (1 - u) ^ (b - 1)

The upper tail of Euler's second beta integral, rewritten through the chart u ↦ u / (1 - u).

theorem TauCeti.integral_Ioo_rpow_one_sub_rpow_tail_eq {a b u0 : ℝ} (ha : 0 < a) (hb : 0 < b) (hu00 : 0 ≤ u0) (hu01 : u0 < 1) : ∫ (u : ℝ) in Set.Ioo u0 1, u ^ (a - 1) * (1 - u) ^ (b - 1) = ProbabilityTheory.beta a b * (1 - regularizedIncompleteBeta a b u0)

The upper tail of the first beta-integral kernel is the total beta mass minus the normalized lower incomplete beta mass.

theorem TauCeti.integral_Ioi_rpow_one_add_rpow_tail_eq {a b u0 : ℝ} (ha : 0 < a) (hb : 0 < b) (hu00 : 0 ≤ u0) (hu01 : u0 < 1) : ∫ (w : ℝ) in Set.Ioi (u0 / (1 - u0)), w ^ (a - 1) * (1 + w) ^ (-(a + b)) = ProbabilityTheory.beta a b * (1 - regularizedIncompleteBeta a b u0)

The upper tail of Euler's second beta integral, expressed by the regularized incomplete beta function.

theorem TauCeti.regularizedIncompleteBeta_symm {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (x : ℝ) : regularizedIncompleteBeta a b x = 1 - regularizedIncompleteBeta b a (1 - x)

The reflection formula I_x(a, b) = 1 - I_{1-x}(b, a), valid at every real argument: the clamping convention makes both sides constant outside [0, 1], so no restriction on x is needed. Positivity of both parameters is needed, however: at a = 0 < b and x < 0 the left side is 0 while the right side is 1, because regularizedIncompleteBeta b 0 vanishes identically.

Boundary parameter values

@[simp]

theorem TauCeti.regularizedIncompleteBeta_one_right {a x : ℝ} (ha : 0 < a) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : regularizedIncompleteBeta a 1 x = x ^ a

At second parameter 1 the beta integrand loses its second factor, and the regularized incomplete beta function is the power x ^ a.

@[simp]

theorem TauCeti.regularizedIncompleteBeta_one_left {b x : ℝ} (hb : 0 < b) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : regularizedIncompleteBeta 1 b x = 1 - (1 - x) ^ b

At first parameter 1 the reflection formula turns TauCeti.regularizedIncompleteBeta_one_right into the complementary power 1 - (1 - x) ^ b.

The unit-step recurrence

theorem TauCeti.regularizedIncompleteBeta_add_one_left {a b x : ℝ} (ha : 0 < a) (hb : 0 < b) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : regularizedIncompleteBeta (a + 1) b x = regularizedIncompleteBeta a b x - x ^ a * (1 - x) ^ b / (a * ProbabilityTheory.beta a b)

The unit-step recurrence in the first parameter, I_x(a + 1, b) = I_x(a, b) - x ^ a * (1 - x) ^ b / (a * Β(a, b)), in the form of DLMF 8.17.20.

The argument is restricted to 0 ≤ x ≤ 1: outside [0, 1] the clamping freezes both regularized values at 0 or at 1 while the subtracted term keeps varying with x, so the displayed formula fails there.

theorem TauCeti.regularizedIncompleteBeta_add_one_right {a b x : ℝ} (ha : 0 < a) (hb : 0 < b) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : regularizedIncompleteBeta a (b + 1) x = regularizedIncompleteBeta a b x + x ^ a * (1 - x) ^ b / (b * ProbabilityTheory.beta a b)

The unit-step recurrence in the second parameter, I_x(a, b + 1) = I_x(a, b) + x ^ a * (1 - x) ^ b / (b * Β(a, b)).

It is the reflection of TauCeti.regularizedIncompleteBeta_add_one_left, and carries the same restriction 0 ≤ x ≤ 1 for the same reason.

theorem TauCeti.regularizedIncompleteBeta_add_one_right_sub_add_one_left {a b x : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : regularizedIncompleteBeta a (b + 1) x - regularizedIncompleteBeta (a + 1) b x = Real.Gamma (a + b + 1) / (Real.Gamma (a + 1) * Real.Gamma (b + 1)) * (x ^ a * (1 - x) ^ b)

The step along the antidiagonal a + b = const, which is the recurrence the binomial tail runs on: I_x(a, b + 1) - I_x(a + 1, b) = Γ(a + b + 1) / (Γ(a + 1) * Γ(b + 1)) * (x ^ a * (1 - x) ^ b).

The coefficient is the generalized binomial coefficient (a + b).choose a, so at natural parameters a = m and b = n - m the right-hand side is the m-th binomial weight (n.choose m) * x ^ m * (1 - x) ^ (n - m).

The first parameter is only assumed nonnegative. At a = 0 the identity reads 1 - I_x(1, b) = (1 - x) ^ b, which holds precisely because TauCeti.regularizedIncompleteBeta takes the value 1 at first parameter 0: the boundary convention is what makes the antidiagonal recurrence start at a = 0.