Exponential moments of noncentral chi-squared laws #
For nonnegative degree k and noncentrality l, the moment-generating function is
(1 - 2 * t) ^ (-(k / 2)) * exp (l * t / (1 - 2 * t)) below 1 / 2.
The exponential-integrability domain is exactly this half-line unless both parameters vanish,
when the law is the point mass at zero and every exponential moment exists.
References #
- N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, second edition, Wiley, 1995, chapter 29.
theorem
TauCeti.Probability.integrable_exp_mul_noncentralChiSquaredMeasure
{k t : ℝ}
(hk : 0 ≤ k)
(l : NNReal)
(ht : t < 2⁻¹)
:
MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (noncentralChiSquaredMeasure k l)
Every exponential moment below 1 / 2 exists, including at the double-zero Dirac boundary.
theorem
TauCeti.Probability.not_integrable_exp_mul_noncentralChiSquaredMeasure
{k t : ℝ}
{l : NNReal}
(hk : 0 ≤ k)
(hne : k ≠ 0 ∨ l ≠ 0)
(ht : 2⁻¹ ≤ t)
:
¬MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (noncentralChiSquaredMeasure k l)
At or above 1 / 2, the exponential integrand is not integrable under any valid
noncentral chi-squared law other than the double-zero Dirac law.
@[simp]
theorem
TauCeti.Probability.integrableExpSet_id_noncentralChiSquaredMeasure
{k : ℝ}
(hk : 0 ≤ k)
(l : NNReal)
:
The exact exponential domain is all of ℝ at the double-zero boundary and (-∞, 1/2)
at every other valid degree and noncentrality.