Euler's beta integrals, in real-valued form

Mathlib defines Euler's beta function ProbabilityTheory.beta by the Gamma quotient, and proves that it is the value of Complex.betaIntegral, the complex-valued interval integral of t ^ (a - 1) * (1 - t) ^ (b - 1) over [0, 1]. This file records the real-variable facts about the real-valued beta integrand t ^ (a - 1) * (1 - t) ^ (b - 1) that a real-analysis consumer needs: its interval integrability on [0, 1], the value Β(a, b) of its integral over [0, 1], the derivative of the kernel t ^ a * (1 - t) ^ b it primitivises, and the splitting of the integrand that raises the second parameter by one. Two parameter identities for Β itself — symmetry and the unit step in the first parameter — are recorded alongside.

It also records Euler's second beta integral, the half-line form ∫ x in Ioi 0, x ^ (a - 1) * (1 + x) ^ (-(a + b)) = Β(a, b), together with its integrability statement, and specialises it to the Cauchy-type kernel (1 + x ^ 2) ^ (-s) on the whole line.

These are the analytic prerequisites of TauCeti/Analysis/SpecialFunctions/IncompleteBeta.lean; TauCeti/Probability/Distributions/Beta/Basic.lean uses the beta integral for its moment formula, and TauCeti/Probability/Distributions/StudentT/Basic.lean normalizes its density with the (1 + x ^ 2) ^ (-s) form of the second integral.

Main results

• TauCeti.intervalIntegrable_rpow_mul_one_sub_rpow — interval integrability of the beta integrand between any two points of [0, 1];
• TauCeti.integral_rpow_mul_one_sub_rpow — Euler's beta integral, ∫ t in 0..1, t ^ (a - 1) * (1 - t) ^ (b - 1) = Β(a, b);
• TauCeti.hasDerivAt_rpow_mul_one_sub_rpow — the derivative of t ^ a * (1 - t) ^ b;
• TauCeti.integral_rpow_mul_one_sub_rpow_add_one_right — raising the second parameter by one splits the integral as a difference;
• TauCeti.integrableOn_rpow_mul_one_add_rpow_iff and TauCeti.integral_rpow_mul_one_add_rpow — Euler's second beta integral and its sharp integrability criterion, ∫ x in Ioi 0, x ^ (a - 1) * (1 + x) ^ (-(a + b)) = Β(a, b);
• TauCeti.abs_deriv_smul_one_add_rpow — the change-of-variables identity relating the first and second beta-integral kernels under the chart u ↦ u / (1 - u);
• TauCeti.integrable_one_add_sq_rpow, TauCeti.integral_one_add_sq_rpow, TauCeti.integrable_one_add_sq_div_rpow, and TauCeti.integral_one_add_sq_div_rpow — the Cauchy-type kernel (1 + x ^ 2 / ν) ^ (-s) is integrable on the line for 0 < ν and 1 / 2 < s, with total mass √ν * Β(1 / 2, s - 1 / 2);
• ProbabilityTheory.beta_comm — symmetry of Β;
• ProbabilityTheory.beta_one_right — the value Β(a, 1) = 1 / a;
• ProbabilityTheory.beta_add_one_left — the unit step Β(a + 1, b) = a / (a + b) * Β(a, b).

Implementation notes

The proof of TauCeti.intervalIntegrable_rpow_mul_one_sub_rpow transposes the argument of Mathlib's Complex.betaIntegral_convergent and Complex.betaIntegral_convergent_left to the real-valued setting: split [0, 1] at 1 / 2 and handle each endpoint singularity with intervalIntegral.intervalIntegrable_rpow' against a factor that is continuous there, obtaining the right half from the left one by the reflection t ↦ 1 - t. The proof of TauCeti.integral_rpow_mul_one_sub_rpow adapts the normalization argument for ProbabilityTheory.betaMeasure in Mathlib, ProbabilityTheory.lintegral_betaPDF_eq_one: descend from Complex.betaIntegral by taking real parts.

Both changes of variables for the second integral are one-dimensional, run through MeasureTheory.integral_image_eq_integral_abs_deriv_smul and its integrability companion. The chart u ↦ u / (1 - u) carries (0, 1) onto (0, ∞) and turns the first integrand into the second; the chart t ↦ √t carries (0, ∞) onto itself and turns (1 + x ^ 2) ^ (-s) into the second integrand with first parameter 1 / 2. Full-line integrability is an instance of Mathlib's integrable_rpow_neg_one_add_norm_sq, and the integral value folds the two halves of the line together with MeasureTheory.integral_comp_abs.

References

• Tau Ceti roadmap, StandardDistributions, Layer 2, "Regularized incomplete beta", for which these are the prerequisites, and Layer 3, Student's t, which needs the second integral.
• NIST Digital Library of Mathematical Functions, §5.12.

theorem TauCeti.intervalIntegrable_rpow_mul_one_sub_rpow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {u v : ℝ} (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : IntervalIntegrable (fun (t : ℝ) => t ^ (a - 1) * (1 - t) ^ (b - 1)) MeasureTheory.volume u v

The integrand t ^ (a - 1) * (1 - t) ^ (b - 1) of Euler's beta integral is interval integrable between any two points of [0, 1]. Both endpoint singularities are integrable precisely because the exponents exceed -1.

theorem TauCeti.integral_rpow_mul_one_sub_rpow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (t : ℝ) in 0..1, t ^ (a - 1) * (1 - t) ^ (b - 1) = ProbabilityTheory.beta a b

Euler's beta integral, in real-valued interval form: for positive parameters the integral of t ^ (a - 1) * (1 - t) ^ (b - 1) over [0, 1] is Β(a, b).

theorem TauCeti.hasDerivAt_rpow_mul_one_sub_rpow (a b : ℝ) {t : ℝ} (ht0 : t ≠ 0 ∨ 1 ≤ a) (ht1 : t ≠ 1 ∨ 1 ≤ b) : HasDerivAt (fun (t : ℝ) => t ^ a * (1 - t) ^ b) (a * (t ^ (a - 1) * (1 - t) ^ b) - b * (t ^ a * (1 - t) ^ (b - 1))) t

The derivative of the kernel t ^ a * (1 - t) ^ b primitivised by the beta integrand. Each endpoint has to be avoided only when the exponent that degenerates there is smaller than 1: t ^ a is differentiable at 0 as soon as 1 ≤ a, and (1 - t) ^ b at 1 as soon as 1 ≤ b.

theorem TauCeti.integral_rpow_mul_one_sub_rpow_add_one_right {a b x : ℝ} (ha : 0 < a) (hb : 0 < b) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ∫ (t : ℝ) in 0..x, t ^ (a - 1) * (1 - t) ^ b = (∫ (t : ℝ) in 0..x, t ^ (a - 1) * (1 - t) ^ (b - 1)) - ∫ (t : ℝ) in 0..x, t ^ a * (1 - t) ^ (b - 1)

Raising the second parameter of the beta integrand by one splits its integral as a difference: off the endpoints t ^ (a - 1) * (1 - t) ^ b = t ^ (a - 1) * (1 - t) ^ (b - 1) - t ^ a * (1 - t) ^ (b - 1).

Euler's second beta integral

theorem TauCeti.abs_deriv_smul_one_add_rpow (a b : ℝ) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : |((1 - u) ^ 2)⁻¹| • ((u / (1 - u)) ^ (a - 1) * (1 + u / (1 - u)) ^ (-(a + b))) = u ^ (a - 1) * (1 - u) ^ (b - 1)

Under the chart u ↦ u / (1 - u) the integrand of Euler's second beta integral becomes the integrand of Euler's first one.

theorem TauCeti.integrableOn_rpow_mul_one_add_rpow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (a - 1) * (1 + x) ^ (-(a + b))) (Set.Ioi 0) MeasureTheory.volume

The integrand of Euler's second beta integral is integrable on the positive half-line whenever both parameters are positive.

theorem TauCeti.integrableOn_rpow_mul_one_add_rpow_iff {a b : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ (a - 1) * (1 + x) ^ (-(a + b))) (Set.Ioi 0) MeasureTheory.volume ↔ 0 < b

The integrand of Euler's second beta integral is integrable on the positive half-line exactly when its tail parameter is positive, provided its exponent at zero is positive.

theorem TauCeti.integral_rpow_mul_one_add_rpow {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (x : ℝ) in Set.Ioi 0, x ^ (a - 1) * (1 + x) ^ (-(a + b)) = ProbabilityTheory.beta a b

Euler's second beta integral: for positive parameters the integral of x ^ (a - 1) * (1 + x) ^ (-(a + b)) over the positive half-line is Β(a, b).

The Cauchy-type kernel (1 + x ^ 2) ^ (-s)

theorem TauCeti.integrable_one_add_sq_rpow {s : ℝ} (hs : 1 / 2 < s) : MeasureTheory.Integrable (fun (x : ℝ) => (1 + x ^ 2) ^ (-s)) MeasureTheory.volume

The Cauchy-type kernel (1 + x ^ 2) ^ (-s) is integrable on the line when 1 / 2 < s.

theorem TauCeti.integral_one_add_sq_rpow {s : ℝ} (hs : 1 / 2 < s) : ∫ (x : ℝ), (1 + x ^ 2) ^ (-s) = ProbabilityTheory.beta (1 / 2) (s - 1 / 2)

The total mass of the Cauchy-type kernel (1 + x ^ 2) ^ (-s) is Β(1/2, s - 1/2).

theorem TauCeti.integrable_one_add_sq_div_rpow {ν s : ℝ} (hν : 0 < ν) (hs : 1 / 2 < s) : MeasureTheory.Integrable (fun (x : ℝ) => (1 + x ^ 2 / ν) ^ (-s)) MeasureTheory.volume

The rescaled Cauchy-type kernel is integrable on the line.

theorem TauCeti.integral_one_add_sq_div_rpow {ν s : ℝ} (hν : 0 < ν) (hs : 1 / 2 < s) : ∫ (x : ℝ), (1 + x ^ 2 / ν) ^ (-s) = √ν * ProbabilityTheory.beta (1 / 2) (s - 1 / 2)

The total mass of a rescaled Cauchy-type kernel. Rescaling by √ν reduces it to Euler's second beta integral.

theorem ProbabilityTheory.beta_comm (a b : ℝ) : beta a b = beta b a

Euler's beta function is symmetric in its two parameters.

@[simp]

theorem ProbabilityTheory.beta_one_right {a : ℝ} (ha : 0 < a) : beta a 1 = 1 / a

Euler's beta function at second parameter 1.

theorem ProbabilityTheory.beta_add_one_left {a b : ℝ} (ha : a ≠ 0) (hab : a + b ≠ 0) : beta (a + 1) b = a / (a + b) * beta a b

The unit step of Euler's beta function in its first parameter.