Further results about the Euler Beta integral

This file is a temporary home for results intended to accompany Mathlib.Analysis.SpecialFunctions.Gamma.Beta.

theorem Complex.intervalIntegrable_betaKernel_scaled {u v : ℂ} (hu : 0 < u.re) (hv : 0 < v.re) {a : ℝ} (ha : 0 ≤ a) : IntervalIntegrable (fun (x : ℝ) => ↑x ^ (u - 1) * (↑a - ↑x) ^ (v - 1)) MeasureTheory.volume 0 a

The scaled Beta kernel is interval-integrable on [0, a] under the usual convergence conditions.

theorem Complex.integral_norm_betaKernel_scaled (u v : ℂ) {a : ℝ} (ha : 0 < a) : ∫ (t : ℝ) in 0..a, ‖↑t ^ (u - 1) * (↑a - ↑t) ^ (v - 1)‖ = a ^ (u.re + v.re - 1) * ∫ (t : ℝ) in 0..1, ‖↑t ^ (u - 1) * (1 - ↑t) ^ (v - 1)‖

Scaling identity for the L¹ norm of the complex Beta kernel. Unlike integrability of the kernel, this pointwise change-of-scale identity needs no conditions on the real parts of the parameters.

theorem Real.integrableOn_Icc_rpow_mul_sub_rpow {a c s : ℝ} (ha : 0 < a) (hc : 0 < c) (hs : 0 ≤ s) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (a - 1) * (s - t) ^ (c - 1)) (Set.Icc 0 s) MeasureTheory.volume

The real Beta kernel is integrable on every nonnegative closed interval.

theorem Real.integrableOn_Icc_rpow_mul_one_sub_rpow {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ (a - 1) * (1 - t) ^ (c - 1)) (Set.Icc 0 1) MeasureTheory.volume

The real Euler beta kernel is integrable on the closed unit interval.

theorem Real.integral_Icc_rpow_mul_one_sub_rpow {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : ∫ (t : ℝ) in Set.Icc 0 1, t ^ (a - 1) * (1 - t) ^ (c - 1) = ProbabilityTheory.beta a c

The real Euler beta integral in set-integral form.

theorem Real.integral_Icc_rpow_mul_sub_rpow {a c s : ℝ} (ha : 0 < a) (hc : 0 < c) (hs : 0 < s) : ∫ (t : ℝ) in Set.Icc 0 s, t ^ (a - 1) * (s - t) ^ (c - 1) = s ^ (a + c - 1) * ProbabilityTheory.beta a c

The scaled real Euler beta integral in set-integral form.

theorem Real.lintegral_Icc_rpow_mul_sub_rpow {a c s : ℝ} (ha : 0 < a) (hc : 0 < c) (hs : 0 < s) : ∫⁻ (x : ℝ) in Set.Icc 0 s, ENNReal.ofReal (x ^ (a - 1) * (s - x) ^ (c - 1)) = ENNReal.ofReal (s ^ (a + c - 1) * ProbabilityTheory.beta a c)

The nonnegative Beta integral on an arbitrary positive interval.

theorem MeasureTheory.integral_Icc_pow_mul_one_sub_pow (a b : ℕ) : ∫ (t : ℝ) in Set.Icc 0 1, t ^ a * (1 - t) ^ b = ↑a.factorial * ↑b.factorial / ↑(a + b + 1).factorial

The beta integral at positive integer parameters, in a form convenient for simplex monomial integrals.