Fisher's F law as a ratio of independent chi-squared variables

Fisher's F law is defined in TauCeti/Probability/Distributions/FisherSnedecor/Basic.lean as the image of betaMeasure (m / 2) (n / 2) under the beta-to-F transformation u ↦ (n / m) * u / (1 - u). This file justifies that definition by identifying the law with the classical ratio it is named for: for independent chi-squared variables U and V with m and n degrees of freedom, the variance ratio (U / m) / (V / n) has the law fisherSnedecorMeasure m n.

The identification is stated in two parametrizations. A chi-squared law with k degrees of freedom is the gamma law of shape k / 2 and rate 1 / 2, and a ratio is unchanged by a common scaling of its two arguments, so the gamma form map_scaled_div_gammaMeasure covers all gamma variables with a common rate, at the price of writing the degrees of freedom as 2 * a and 2 * b. The chi-squared form map_scaled_div_chiSquaredMeasure is its specialisation to the classical parameters, and is the statement to use for a variance ratio.

Main results

• TauCeti.Probability.map_scaled_div_gammaMeasure — the pushforward of a product of gamma laws with a common rate along the scaled quotient is Fisher's F law;
• TauCeti.Probability.map_scaled_div_chiSquaredMeasure — the same statement for chi-squared laws, in the classical degrees-of-freedom parametrization;
• TauCeti.Probability.hasLaw_fisherSnedecor_of_gammaMeasure and TauCeti.Probability.hasLaw_fisherSnedecor_of_chiSquared — the random-variable forms.

References

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

The pushforward of a product of gamma laws

theorem TauCeti.Probability.map_scaled_div_gammaMeasure {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) : MeasureTheory.Measure.map (fun (z : ℝ × ℝ) => z.1 / (2 * a) / (z.2 / (2 * b))) ((ProbabilityTheory.gammaMeasure a r).prod (ProbabilityTheory.gammaMeasure b r)) = fisherSnedecorMeasure (2 * a) (2 * b)

The variance ratio of two independent gamma variables with a common positive rate has Fisher's F law with twice their shape parameters as degrees of freedom. The common rate cancels, so it does not appear in the conclusion.

theorem TauCeti.Probability.map_scaled_div_chiSquaredMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : MeasureTheory.Measure.map (fun (z : ℝ × ℝ) => z.1 / m / (z.2 / n)) ((chiSquaredMeasure m).prod (chiSquaredMeasure n)) = fisherSnedecorMeasure m n

The variance ratio of two independent chi-squared variables with positive degrees of freedom m and n has the law fisherSnedecorMeasure m n.

This is the classical description of Fisher's F law, and the reason for the name of TauCeti.Probability.fisherSnedecorMeasure.

Random-variable forms

theorem TauCeti.Probability.hasLaw_fisherSnedecor_of_gammaMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.gammaMeasure b r) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω / (2 * a) / (Y ω / (2 * b))) (fisherSnedecorMeasure (2 * a) (2 * b)) P

If X and Y are independent gamma variables with a common positive rate and shapes a and b, then (X / (2 * a)) / (Y / (2 * b)) has Fisher's F law with 2 * a and 2 * b degrees of freedom.

theorem TauCeti.Probability.hasLaw_fisherSnedecor_of_chiSquared {m n : ℝ} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} (hm : 0 < m) (hn : 0 < n) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (chiSquaredMeasure m) P) (hY : ProbabilityTheory.HasLaw Y (chiSquaredMeasure n) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω / m / (Y ω / n)) (fisherSnedecorMeasure m n) P

If X and Y are independent chi-squared variables with positive degrees of freedom m and n, then the variance ratio (X / m) / (Y / n) has the law fisherSnedecorMeasure m n.