The cumulative distribution function of Fisher's F law

For positive degrees of freedom m and n, the cumulative distribution function of fisherSnedecorMeasure m n is 0 on the nonpositive half-line and, at x > 0, the regularized incomplete beta function I_{m / 2, n / 2} at m * x / (n + m * x), the inverse of the beta-to-F map. This is the beta distribution function read through that inverse, in the regularized-incomplete-beta convention of the beta API.

Main results

• cdf_fisherSnedecorMeasure_eq — the closed-form cumulative distribution function.

References

• N. L. Johnson, S. Kotz, and N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley (1995), chapter 27.

theorem TauCeti.Probability.cdf_fisherSnedecorMeasure_eq {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (x : ℝ) : ↑(ProbabilityTheory.cdf (fisherSnedecorMeasure m n)) x = if x ≤ 0 then 0 else regularizedIncompleteBeta (m / 2) (n / 2) (m * x / (n + m * x))

For positive degrees of freedom, the cdf is 0 when x ≤ 0 and is the regularized incomplete beta function at m * x / (n + m * x) when 0 < x.