The square chart for weighted half-line integrals of Student's t law

The substitution w = z ^ 2 / ν reduces weighted integrals of the even Student t density over the positive half-line to Euler integrals on (0, ∞). This file collects the Student-t beta-kernel normal form of the transformed density and the kernel itself; the general square-chart facts live in TauCeti/Analysis/Calculus/RealCharts.lean.

Weighted half-line integrals

@[reducible, inline]

noncomputable abbrev TauCeti.Probability.studentTBetaKernel (ν q w : ℝ) : ℝ

The kernel on the positive half-line after the substitution w = x ^ 2 / ν: w ^ ((q - 1) / 2) * (1 + w) ^ (-((ν + 1) / 2)).

Equations

• TauCeti.Probability.studentTBetaKernel ν q w = w ^ ((q - 1) / 2) * (1 + w) ^ (-((ν + 1) / 2))

theorem TauCeti.Probability.abs_deriv_smul_studentTPDFReal {ν : ℝ} (hν : 0 < ν) (q : ℝ) {z : ℝ} (hz : 0 < z) : |2 * z / ν| • (Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * ν ^ ((q + 1) / 2) / 2 * studentTBetaKernel ν q (z ^ 2 / ν)) = studentTPDFReal ν z * z ^ q

Under the chart z ↦ z ^ 2 / ν, the weighted Student t density becomes the normalized beta kernel on the positive half-line.