Moments of Fisher's F distribution

This file establishes the sharp moment and exponential-integrability theory of the Fisher--Snedecor law: the mean, the second raw moment, the variance, the exact integrability thresholds 2 < n and 4 < n at which the first two moments diverge, and the exact exponential-integrability domain. The moment results come from a file-internal computation of the natural moment of order q, which exists exactly when 2 * q < n and is then a quotient of beta functions. Since the law is positive and has only polynomial decay, its exponential moments exist exactly at nonpositive rates.

Main results

• integrable_id_fisherSnedecorMeasure_iff and integrable_sq_fisherSnedecorMeasure_iff give the two sharp integrability thresholds, hence also the divergence at and below them.
• integral_id_fisherSnedecorMeasure computes the mean.
• integral_sq_fisherSnedecorMeasure computes the second raw moment.
• variance_id_fisherSnedecorMeasure computes the variance.
• integrableExpSet_id_fisherSnedecorMeasure identifies the exponential-integrability domain as the nonpositive half-line.

References

• N. L. Johnson, S. Kotz, and N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley (1995), chapter 27.
• The formal beta-kernel argument follows TauCeti.Probability.Distributions.StudentT.Moments.

@[simp]

theorem TauCeti.Probability.integrable_id_fisherSnedecorMeasure_iff {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : MeasureTheory.Integrable id (fisherSnedecorMeasure m n) ↔ 2 < n

The identity is integrable under a valid Fisher--Snedecor law exactly above two denominator degrees of freedom.

@[simp]

theorem TauCeti.Probability.integrable_sq_fisherSnedecorMeasure_iff {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (fisherSnedecorMeasure m n) ↔ 4 < n

Squaring is integrable under a valid Fisher--Snedecor law exactly above four denominator degrees of freedom.

Exponential moments

theorem TauCeti.Probability.integrable_exp_mul_id_fisherSnedecorMeasure_of_nonpos (m n : ℝ) {t : ℝ} (ht : t ≤ 0) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (fisherSnedecorMeasure m n)

Every nonpositive exponential rate is integrable under a Fisher--Snedecor measure, including the zero measure produced by invalid parameters.

theorem TauCeti.Probability.not_integrable_exp_mul_id_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) {t : ℝ} (ht : 0 < t) : ¬MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (fisherSnedecorMeasure m n)

Positive exponential rates are not integrable under a valid Fisher--Snedecor law.

@[simp]

theorem TauCeti.Probability.integrable_exp_mul_id_fisherSnedecorMeasure_iff {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (fisherSnedecorMeasure m n) ↔ t ≤ 0

The exponential of a multiple of the identity is integrable under a valid Fisher--Snedecor law exactly when the rate is nonpositive.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : ProbabilityTheory.integrableExpSet id (fisherSnedecorMeasure m n) = Set.Iic 0

The exact exponential-integrability domain of the identity under a valid Fisher--Snedecor law is the nonpositive half-line.

@[simp]

theorem TauCeti.Probability.integral_id_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 2 < n) : ∫ (x : ℝ), x ∂fisherSnedecorMeasure m n = n / (n - 2)

The mean of a Fisher--Snedecor law is n / (n - 2) when 2 < n.

@[simp]

theorem TauCeti.Probability.integral_sq_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 4 < n) : ∫ (x : ℝ), x ^ 2 ∂fisherSnedecorMeasure m n = n ^ 2 * (m + 2) / (m * (n - 2) * (n - 4))

The second raw moment of a Fisher--Snedecor law is n ^ 2 * (m + 2) / (m * (n - 2) * (n - 4)) when 4 < n.

@[simp]

theorem TauCeti.Probability.variance_id_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 4 < n) : ProbabilityTheory.variance id (fisherSnedecorMeasure m n) = 2 * n ^ 2 * (m + n - 2) / (m * (n - 2) ^ 2 * (n - 4))

The variance of a Fisher--Snedecor law is 2 * n ^ 2 * (m + n - 2) / (m * (n - 2) ^ 2 * (n - 4)) when 4 < n.