Fisher's F distribution

Main definitions

• fisherSnedecorMeasure — the Fisher--Snedecor probability measure.
• fisherSnedecorPDFReal and fisherSnedecorPDF — its real- and extended-nonnegative-valued densities.
• fisherSnedecorMap — the beta-to-F transformation.
• fisherSnedecorMapInv — its inverse on the positive half-line.

Main results

• fisherSnedecorMeasure_eq_map — the beta pushforward characterization.
• isProbabilityMeasure_fisherSnedecorMeasure_iff — the exact parameter range for a probability measure.
• fisherSnedecorMap_image_Ioo — the image of the open unit interval.
• fisherSnedecorMap_strictMonoOn — strict monotonicity below one.
• fisherSnedecorMapInv_map and fisherSnedecorMap_mapInv — the inverse identities.
• fisherSnedecorMap_div_add — the beta-to-F image of a ratio-to-sum is the scaled quotient.
• ae_mem_Ioi_fisherSnedecorMeasure — positivity almost surely.
• fisherSnedecorMeasure_eq_withDensity — the density representation with respect to Lebesgue measure.
• integrable_fisherSnedecorMeasure_iff and integral_fisherSnedecorMeasure_eq — integrability and integration transferred to the real density.
• hasPDF_of_hasLaw_fisherSnedecorMeasure and rnDeriv_fisherSnedecorMeasure — the random-variable and Radon--Nikodym density interfaces.

This file begins the elementary API for Fisher's F law. For positive degrees of freedom m and n, it realizes the law as the image of betaMeasure (m / 2) (n / 2) under u ↦ (n / m) * u / (1 - u). This gives a probability measure without introducing a second probability-law abstraction. The density is derived from this pushforward by the same beta-to-F change of variables, rather than being used as a second definition of the law.

The change of variables is useful in its own right: the inverse map on the positive half-line is x ↦ m * x / (n + m * x). The cumulative distribution function, which reads the beta distribution function at this inverse, is in TauCeti.Probability.Distributions.FisherSnedecor.Cdf.

References

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

The beta-to-F transformation

noncomputable def TauCeti.Probability.fisherSnedecorMap (m n u : ℝ) : ℝ

The formula for the transformation from a beta variable to an F variable.

For positive m and n, this function is strictly monotone on Iio 1 and maps Ioo 0 1 onto Ioi 0.

theorem TauCeti.Probability.fisherSnedecorMap_def (m n u : ℝ) : fisherSnedecorMap m n u = n / m * u / (1 - u)

The defining formula for fisherSnedecorMap.

noncomputable def TauCeti.Probability.fisherSnedecorMapInv (m n x : ℝ) : ℝ

The formula for the inverse transformation on the positive half-line.

For positive m and n, this is the inverse of fisherSnedecorMap m n between Ioi 0 and Ioo 0 1.

theorem TauCeti.Probability.fisherSnedecorMapInv_def (m n x : ℝ) : fisherSnedecorMapInv m n x = m * x / (n + m * x)

The defining formula for fisherSnedecorMapInv.

noncomputable def TauCeti.Probability.fisherSnedecorMeasure (m n : ℝ) : MeasureTheory.Measure ℝ

The Fisher--Snedecor law with numerator degrees of freedom m and denominator degrees of freedom n. It is the law of (U / m) / (V / n) for independent chi-squared variables with degrees of freedom m and n; it is the zero measure unless 0 < m and 0 < n.

@[simp]

theorem TauCeti.Probability.fisherSnedecorMeasure_of_not_pos {m n : ℝ} (h : ¬(0 < m ∧ 0 < n)) : fisherSnedecorMeasure m n = 0

For invalid degrees of freedom, the Fisher--Snedecor measure is zero.

theorem TauCeti.Probability.fisherSnedecorMeasure_eq_map {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : fisherSnedecorMeasure m n = MeasureTheory.Measure.map (fisherSnedecorMap m n) (ProbabilityTheory.betaMeasure (m / 2) (n / 2))

For positive degrees of freedom, the Fisher--Snedecor measure is the beta-to-F pushforward.

theorem TauCeti.Probability.isProbabilityMeasure_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : MeasureTheory.IsProbabilityMeasure (fisherSnedecorMeasure m n)

The Fisher--Snedecor measure is a probability measure for positive degrees of freedom.

@[simp]

theorem TauCeti.Probability.isProbabilityMeasure_fisherSnedecorMeasure_iff {m n : ℝ} : MeasureTheory.IsProbabilityMeasure (fisherSnedecorMeasure m n) ↔ 0 < m ∧ 0 < n

The Fisher--Snedecor measure is a probability measure exactly when both degrees of freedom are positive.

theorem TauCeti.Probability.measurable_fisherSnedecorMap (m n : ℝ) : Measurable (fisherSnedecorMap m n)

The beta-to-F transformation is measurable for all parameter values.

theorem TauCeti.Probability.measurable_fisherSnedecorMapInv (m n : ℝ) : Measurable (fisherSnedecorMapInv m n)

The beta-to-F inverse transformation is measurable for all parameter values.

Support and the inverse

theorem TauCeti.Probability.fisherSnedecorMap_mem_Ioi {m n : ℝ} (hm : 0 < m) (hn : 0 < n) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : fisherSnedecorMap m n u ∈ Set.Ioi 0

For positive degrees of freedom, the beta-to-F map sends Ioo 0 1 into Ioi 0.

theorem TauCeti.Probability.fisherSnedecorMap_strictMonoOn {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : StrictMonoOn (fisherSnedecorMap m n) (Set.Iio 1)

For positive degrees of freedom, the beta-to-F map is strictly monotone on Iio 1.

theorem TauCeti.Probability.hasDerivAt_fisherSnedecorMap (m n : ℝ) {u : ℝ} (hu : u ≠ 1) : HasDerivAt (fisherSnedecorMap m n) (n / m * ((1 - u) ^ 2)⁻¹) u

The derivative of the beta-to-F transformation away from its pole at one.

@[simp]

theorem TauCeti.Probability.fisherSnedecorMapInv_map {m n : ℝ} (hm : m ≠ 0) (hn : n ≠ 0) {u : ℝ} (hu : u ≠ 1) : fisherSnedecorMapInv m n (fisherSnedecorMap m n u) = u

If m ≠ 0, n ≠ 0, and u ≠ 1, the inverse transformation after the beta-to-F map is the identity.

@[simp]

theorem TauCeti.Probability.fisherSnedecorMap_mapInv {m n : ℝ} (hm : m ≠ 0) (hn : n ≠ 0) {x : ℝ} (hden : n + m * x ≠ 0) : fisherSnedecorMap m n (fisherSnedecorMapInv m n x) = x

If m ≠ 0, n ≠ 0, and n + m * x ≠ 0, the beta-to-F map after the inverse transformation is the identity.

@[simp]

theorem TauCeti.Probability.fisherSnedecorMap_div_add {m n u v : ℝ} (huv : u + v ≠ 0) : fisherSnedecorMap m n (u / (u + v)) = u / m / (v / n)

If u + v ≠ 0, the beta-to-F transformation with m and n degrees of freedom sends the ratio-to-sum u / (u + v) to the variance ratio (u / m) / (v / n); equivalently, it inverts the passage from a variance ratio to the fraction of the total that its numerator carries.

theorem TauCeti.Probability.fisherSnedecorMapInv_mem_Ioo {m n : ℝ} (hm : 0 < m) (hn : 0 < n) {x : ℝ} (hx : 0 < x) : fisherSnedecorMapInv m n x ∈ Set.Ioo 0 1

For positive degrees of freedom, the inverse transformation maps Ioi 0 into Ioo 0 1.

theorem TauCeti.Probability.fisherSnedecorMap_image_Ioo {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : fisherSnedecorMap m n '' Set.Ioo 0 1 = Set.Ioi 0

For positive degrees of freedom, the beta-to-F map sends Ioo 0 1 onto Ioi 0.

theorem TauCeti.Probability.ae_mem_Ioi_fisherSnedecorMeasure (m n : ℝ) : ∀ᵐ (x : ℝ) ∂fisherSnedecorMeasure m n, x ∈ Set.Ioi 0

The Fisher--Snedecor law is almost surely positive, including vacuously for invalid parameters.

Density

noncomputable def TauCeti.Probability.fisherSnedecorPDFReal (m n x : ℝ) : ℝ

The real-valued Fisher--Snedecor density with numerator degrees of freedom m and denominator degrees of freedom n.

It is zero unless both parameters and the sample point are positive.

noncomputable def TauCeti.Probability.fisherSnedecorPDF (m n x : ℝ) : ENNReal

The Fisher--Snedecor density, valued in ℝ≥0∞.

theorem TauCeti.Probability.fisherSnedecorPDF_eq_ofReal (m n x : ℝ) : fisherSnedecorPDF m n x = ENNReal.ofReal (fisherSnedecorPDFReal m n x)

The ℝ≥0∞-valued Fisher--Snedecor density is the nonnegative coercion of its real-valued version.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDFReal_of_pos {m n x : ℝ} (hm : 0 < m) (hn : 0 < n) (hx : 0 < x) : fisherSnedecorPDFReal m n x = Real.Gamma ((m + n) / 2) / (Real.Gamma (m / 2) * Real.Gamma (n / 2)) * (m / n) ^ (m / 2) * x ^ (m / 2 - 1) * (1 + m * x / n) ^ (-((m + n) / 2))

The real density has its usual formula at valid parameters and a positive point.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDFReal_of_nonpos {x : ℝ} (hx : x ≤ 0) (m n : ℝ) : fisherSnedecorPDFReal m n x = 0

The real density vanishes on the nonpositive half-line.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDFReal_of_not_pos {m n : ℝ} (h : ¬(0 < m ∧ 0 < n)) (x : ℝ) : fisherSnedecorPDFReal m n x = 0

The real density vanishes unless both degrees of freedom are positive.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDF_of_pos {m n x : ℝ} (hm : 0 < m) (hn : 0 < n) (hx : 0 < x) : fisherSnedecorPDF m n x = ENNReal.ofReal (Real.Gamma ((m + n) / 2) / (Real.Gamma (m / 2) * Real.Gamma (n / 2)) * (m / n) ^ (m / 2) * x ^ (m / 2 - 1) * (1 + m * x / n) ^ (-((m + n) / 2)))

The ℝ≥0∞-valued density has its usual formula at valid parameters and a positive point.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDF_of_nonpos {x : ℝ} (hx : x ≤ 0) (m n : ℝ) : fisherSnedecorPDF m n x = 0

The ℝ≥0∞-valued density vanishes on the nonpositive half-line.

@[simp]

theorem TauCeti.Probability.fisherSnedecorPDF_of_not_pos {m n : ℝ} (h : ¬(0 < m ∧ 0 < n)) (x : ℝ) : fisherSnedecorPDF m n x = 0

The ℝ≥0∞-valued density vanishes unless both degrees of freedom are positive.

theorem TauCeti.Probability.fisherSnedecorPDFReal_nonneg (m n x : ℝ) : 0 ≤ fisherSnedecorPDFReal m n x

The real-valued Fisher--Snedecor density is nonnegative.

@[simp]

theorem TauCeti.Probability.toReal_fisherSnedecorPDF (m n x : ℝ) : (fisherSnedecorPDF m n x).toReal = fisherSnedecorPDFReal m n x

Converting the Fisher--Snedecor density back to ℝ recovers its real-valued version.

theorem TauCeti.Probability.measurable_fisherSnedecorPDFReal (m n : ℝ) : Measurable (fisherSnedecorPDFReal m n)

The real Fisher--Snedecor density is measurable in the sample point.

theorem TauCeti.Probability.measurable_fisherSnedecorPDF (m n : ℝ) : Measurable (fisherSnedecorPDF m n)

The ℝ≥0∞-valued Fisher--Snedecor density is measurable in the sample point.

theorem TauCeti.Probability.indicator_Ioi_fisherSnedecorPDF (m n : ℝ) : (Set.Ioi 0).indicator (fisherSnedecorPDF m n) = fisherSnedecorPDF m n

The Fisher--Snedecor density is supported on the positive half-line.

theorem TauCeti.Probability.fisherSnedecorPDFReal_eq_scaled_beta {m n x : ℝ} (hm : 0 < m) (hn : 0 < n) (hx : 0 < x) : fisherSnedecorPDFReal m n x = m / n * (1 / ProbabilityTheory.beta (m / 2) (n / 2)) * (m * x / n) ^ (m / 2 - 1) * (1 + m * x / n) ^ (-((m + n) / 2))

The classical Fisher density in the scaled beta-prime form used by its change of variables.

theorem TauCeti.Probability.fisherSnedecorMeasure_eq_withDensity (m n : ℝ) : fisherSnedecorMeasure m n = MeasureTheory.volume.withDensity (fisherSnedecorPDF m n)

The density of the Fisher--Snedecor law, including the zero density at invalid parameters.

theorem TauCeti.Probability.integrable_fisherSnedecorMeasure_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m n : ℝ) {g : ℝ → E} : MeasureTheory.Integrable g (fisherSnedecorMeasure m n) ↔ MeasureTheory.Integrable (fun (x : ℝ) => fisherSnedecorPDFReal m n x • g x) MeasureTheory.volume

Integrability transfer. A function is integrable against a Fisher--Snedecor law exactly when its density-weighted version is Lebesgue integrable. This holds at every parameter, the zero measure included.

theorem TauCeti.Probability.integral_fisherSnedecorMeasure_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (m n : ℝ) (g : ℝ → E) : ∫ (x : ℝ), g x ∂fisherSnedecorMeasure m n = ∫ (x : ℝ), fisherSnedecorPDFReal m n x • g x

Integral transfer. An integral against a Fisher--Snedecor law is the density-weighted Lebesgue integral. This holds at every parameter, the zero measure included.

theorem TauCeti.Probability.hasPDF_of_hasLaw_fisherSnedecorMeasure {m n : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (fisherSnedecorMeasure m n) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random variable with a Fisher--Snedecor law has the corresponding density.

theorem TauCeti.Probability.pdf_eq_fisherSnedecorPDF_of_hasLaw_fisherSnedecorMeasure {m n : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (fisherSnedecorMeasure m n) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] fisherSnedecorPDF m n

The density of a random variable with a Fisher--Snedecor law is fisherSnedecorPDF.

theorem TauCeti.Probability.rnDeriv_fisherSnedecorMeasure (m n : ℝ) : (fisherSnedecorMeasure m n).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] fisherSnedecorPDF m n

The Radon--Nikodym derivative of a Fisher--Snedecor law against Lebesgue measure.

@[simp]

theorem TauCeti.Probability.support_fisherSnedecorMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) : (fisherSnedecorMeasure m n).support = Set.Ici 0

For positive degrees of freedom the topological support of Fisher's F law is the closed nonnegative half-line.