Noncentral F laws

For positive degrees of freedom m and n and noncentrality l ≥ 0, the noncentral F law is the law of the variance ratio (U / m) / (V / n) of independent variables U and V, where U is noncentral chi-squared with degree m and noncentrality l and V is central chi-squared with degree n. Invalid degrees give the zero measure.

Since the noncentral chi-squared law is a Poisson mixture of central chi-squared laws, the noncentral F law is the Poisson mixture, with weights of rate l / 2, of the scaled central F laws ((m + 2 * j) / m) • F(m + 2 * j, n). This presentation is the route to the density, distribution function, quantile and moments of the family.

Main definitions

• TauCeti.Probability.noncentralFMeasure — the noncentral F law.

Main results

• TauCeti.Probability.isProbabilityMeasure_noncentralFMeasure — normalization.
• TauCeti.Probability.noncentralFMeasure_eq_sum and TauCeti.Probability.noncentralFMeasure_eq_bind — the Poisson mixture of scaled central F laws.
• TauCeti.Probability.noncentralFMeasure_zero_noncentrality — zero noncentrality gives Fisher's F law.
• TauCeti.Probability.absolutelyContinuous_noncentralFMeasure — the law has a density with respect to Lebesgue measure.
• TauCeti.Probability.support_noncentralFMeasure — the topological support is [0, ∞).
• TauCeti.Probability.measurable_noncentralFMeasure — joint parameter measurability.
• TauCeti.Probability.hasLaw_noncentralF_of_noncentralChiSquared — the random-variable form of the defining ratio.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, second edition, Wiley, 1995, chapter 30.

noncomputable def TauCeti.Probability.noncentralFMeasure (m n : ℝ) (l : NNReal) : MeasureTheory.Measure ℝ

The noncentral F law with numerator degree m, denominator degree n and noncentrality l: the law of (U / m) / (V / n) for independent U with law noncentralChiSquaredMeasure m l and V with law chiSquaredMeasure n. It is the zero measure unless 0 < m and 0 < n.

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

For positive degrees, the noncentral F law is the defining variance-ratio pushforward.

@[simp]

theorem TauCeti.Probability.noncentralFMeasure_of_not_pos {m n : ℝ} (h : ¬(0 < m ∧ 0 < n)) (l : NNReal) : noncentralFMeasure m n l = 0

For invalid degrees, the noncentral F measure is zero.

theorem TauCeti.Probability.isProbabilityMeasure_noncentralFMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) : MeasureTheory.IsProbabilityMeasure (noncentralFMeasure m n l)

The noncentral F law is a probability measure for positive degrees.

@[simp]

theorem TauCeti.Probability.isProbabilityMeasure_noncentralFMeasure_iff {m n : ℝ} {l : NNReal} : MeasureTheory.IsProbabilityMeasure (noncentralFMeasure m n l) ↔ 0 < m ∧ 0 < n

The noncentral F measure is a probability measure exactly when both degrees are positive.

instance TauCeti.Probability.isFiniteMeasure_noncentralFMeasure (m n : ℝ) (l : NNReal) : MeasureTheory.IsFiniteMeasure (noncentralFMeasure m n l)

The noncentral F law is a finite measure for every choice of parameters.

The Poisson mixture of scaled central F laws

theorem TauCeti.Probability.noncentralFMeasure_eq_sum {m n : ℝ} (hm : 0 < m) (l : NNReal) : noncentralFMeasure m n l = MeasureTheory.Measure.sum fun (j : ℕ) => (ProbabilityTheory.poissonMeasure (l / 2)) {j} • MeasureTheory.Measure.map (fun (x : ℝ) => (m + 2 * ↑j) / m * x) (fisherSnedecorMeasure (m + 2 * ↑j) n)

The noncentral F law is the Poisson-weighted sum, with weights of rate l / 2, of the central F laws F(m + 2 * j, n) scaled by (m + 2 * j) / m. For n ≤ 0 both sides are zero.

theorem TauCeti.Probability.noncentralFMeasure_eq_bind {m n : ℝ} (hm : 0 < m) (l : NNReal) : noncentralFMeasure m n l = (ProbabilityTheory.poissonMeasure (l / 2)).bind fun (j : ℕ) => MeasureTheory.Measure.map (fun (x : ℝ) => (m + 2 * ↑j) / m * x) (fisherSnedecorMeasure (m + 2 * ↑j) n)

The noncentral F law as a Measure.bind mixture of scaled central F laws over the Poisson law of rate l / 2.

theorem TauCeti.Probability.noncentralFMeasure_apply {m n : ℝ} (hm : 0 < m) (l : NNReal) (s : Set ℝ) : (noncentralFMeasure m n l) s = ∑' (j : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)) {j} * (MeasureTheory.Measure.map (fun (x : ℝ) => (m + 2 * ↑j) / m * x) (fisherSnedecorMeasure (m + 2 * ↑j) n)) s

Set evaluation as an extended-real Poisson series; the formula holds for every set.

theorem TauCeti.Probability.lintegral_noncentralFMeasure {m n : ℝ} (hm : 0 < m) (l : NNReal) (f : ℝ → ENNReal) : ∫⁻ (x : ℝ), f x ∂noncentralFMeasure m n l = ∑' (j : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)) {j} * ∫⁻ (x : ℝ), f ((m + 2 * ↑j) / m * x) ∂fisherSnedecorMeasure (m + 2 * ↑j) n

Nonnegative integration against the noncentral F law can be performed component by component, without measurability, finiteness or integrability assumptions on the observable.

@[simp]

theorem TauCeti.Probability.noncentralFMeasure_zero_noncentrality (m n : ℝ) : noncentralFMeasure m n 0 = fisherSnedecorMeasure m n

At zero noncentrality the noncentral F law is Fisher's F law, for every pair of degrees.

theorem TauCeti.Probability.smul_fisherSnedecorMeasure_le_noncentralFMeasure (m n : ℝ) (l : NNReal) : ENNReal.ofReal (Real.exp (-↑l / 2)) • fisherSnedecorMeasure m n ≤ noncentralFMeasure m n l

The noncentral F law dominates its Poisson-zero component, the central F law with the same degrees weighted by exp (-l / 2), for every choice of parameters.

Support and absolute continuity

theorem TauCeti.Probability.ae_pos_noncentralFMeasure (m n : ℝ) (l : NNReal) : ∀ᵐ (x : ℝ) ∂noncentralFMeasure m n l, 0 < x

A noncentral F variable is positive almost surely, for every choice of parameters.

theorem TauCeti.Probability.absolutelyContinuous_noncentralFMeasure (m n : ℝ) (l : NNReal) : (noncentralFMeasure m n l).AbsolutelyContinuous MeasureTheory.volume

The noncentral F law is absolutely continuous with respect to Lebesgue measure, for every choice of parameters.

instance TauCeti.Probability.nullSingletonClass_noncentralFMeasure (m n : ℝ) (l : NNReal) : MeasureTheory.NullSingletonClass (noncentralFMeasure m n l)

The noncentral F law has no atoms, for every choice of parameters.

@[simp]

theorem TauCeti.Probability.support_noncentralFMeasure {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) : (noncentralFMeasure m n l).support = Set.Ici 0

For positive degrees the topological support is the closed nonnegative half-line, although the variable is positive almost surely.

Parameter measurability

theorem TauCeti.Probability.measurable_noncentralFMeasure : Measurable fun (p : ℝ × ℝ × NNReal) => noncentralFMeasure p.1 p.2.1 p.2.2

The full totalized noncentral F family is jointly measurable in its two degrees and its noncentrality.

Random-variable forms

theorem TauCeti.Probability.hasLaw_noncentralF_of_noncentralChiSquared {m n : ℝ} {l : NNReal} {Ω : 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 (noncentralChiSquaredMeasure m l) P) (hY : ProbabilityTheory.HasLaw Y (chiSquaredMeasure n) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω / m / (Y ω / n)) (noncentralFMeasure m n l) P

If X is noncentral chi-squared with degree m and noncentrality l, and Y is an independent central chi-squared variable with degree n, then the variance ratio (X / m) / (Y / n) has the noncentral F law.

theorem TauCeti.Probability.hasPDF_of_hasLaw_noncentralFMeasure {m n : ℝ} {l : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (noncentralFMeasure m n l) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A variable with a noncentral F law has a probability density function with respect to Lebesgue measure.