Densities of noncentral F laws

The noncentral F density is a convergent Poisson series of scaled central F densities. The scale in each summand is essential: the numerator of the defining ratio is divided by the original numerator degree, rather than the degree of that central component.

The real and extended nonnegative densities vanish at nonpositive arguments and at invalid degrees. Their weighted Lebesgue measure is the ratio law, giving normalization and the Radon–Nikodym and random-variable density identities.

References

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

noncomputable def TauCeti.Probability.noncentralFPDFReal (m n : ℝ) (l : NNReal) (x : ℝ) : ℝ

The noncentral F density as a Poisson series of scaled central F densities. Invalid degrees give zero.

noncomputable def TauCeti.Probability.noncentralFPDF (m n : ℝ) (l : NNReal) (x : ℝ) : ENNReal

The extended nonnegative density of the noncentral F law.

theorem TauCeti.Probability.noncentralFPDF_eq_ofReal (m n : ℝ) (l : NNReal) (x : ℝ) : noncentralFPDF m n l x = ENNReal.ofReal (noncentralFPDFReal m n l x)

The extended density is the nonnegative coercion of the real density.

theorem TauCeti.Probability.summable_poisson_mul_scaled_fisherSnedecorPDFReal {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) (x : ℝ) : Summable fun (j : ℕ) => (ProbabilityTheory.poissonMeasure (l / 2)).real {j} * (m / (m + 2 * ↑j)) * fisherSnedecorPDFReal (m + 2 * ↑j) n (m * x / (m + 2 * ↑j))

The Poisson series of scaled central F densities converges at every real argument.

theorem TauCeti.Probability.noncentralFPDFReal_of_pos {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) (x : ℝ) : noncentralFPDFReal m n l x = ∑' (j : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)).real {j} * (m / (m + 2 * ↑j)) * fisherSnedecorPDFReal (m + 2 * ↑j) n (m * x / (m + 2 * ↑j))

The defining convergent density series at positive degrees.

@[simp]

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

The chosen real density vanishes at invalid degrees.

@[simp]

theorem TauCeti.Probability.noncentralFPDFReal_of_nonpos {x : ℝ} (hx : x ≤ 0) (m n : ℝ) (l : NNReal) : noncentralFPDFReal m n l x = 0

The chosen real density vanishes at nonpositive arguments.

theorem TauCeti.Probability.noncentralFPDFReal_nonneg (m n : ℝ) (l : NNReal) (x : ℝ) : 0 ≤ noncentralFPDFReal m n l x

The real density is nonnegative at all parameters and arguments.

theorem TauCeti.Probability.noncentralFPDFReal_pos {m n x : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) (hx : 0 < x) : 0 < noncentralFPDFReal m n l x

The real density is strictly positive on the positive half-line at valid degrees.

@[simp]

theorem TauCeti.Probability.noncentralFPDFReal_zero_noncentrality (m n x : ℝ) : noncentralFPDFReal m n 0 x = fisherSnedecorPDFReal m n x

Zero noncentrality recovers the central F density, including invalid degrees.

@[simp]

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

Invalid degrees have zero extended density.

@[simp]

theorem TauCeti.Probability.noncentralFPDF_of_nonpos {x : ℝ} (hx : x ≤ 0) (m n : ℝ) (l : NNReal) : noncentralFPDF m n l x = 0

The extended density vanishes at nonpositive arguments.

@[simp]

theorem TauCeti.Probability.noncentralFPDF_zero_noncentrality (m n x : ℝ) : noncentralFPDF m n 0 x = fisherSnedecorPDF m n x

Zero noncentrality recovers the central extended density.

@[simp]

theorem TauCeti.Probability.toReal_noncentralFPDF (m n : ℝ) (l : NNReal) (x : ℝ) : (noncentralFPDF m n l x).toReal = noncentralFPDFReal m n l x

Converting the extended density to a real number recovers the real density.

theorem TauCeti.Probability.measurable_uncurry_noncentralFPDFReal : Measurable fun (p : (ℝ × ℝ × NNReal) × ℝ) => noncentralFPDFReal p.1.1 p.1.2.1 p.1.2.2 p.2

Joint measurability of the real density in both degrees, noncentrality and argument.

theorem TauCeti.Probability.measurable_uncurry_noncentralFPDF : Measurable fun (p : (ℝ × ℝ × NNReal) × ℝ) => noncentralFPDF p.1.1 p.1.2.1 p.1.2.2 p.2

Joint measurability of the extended density.

theorem TauCeti.Probability.measurable_noncentralFPDFReal (m n : ℝ) (l : NNReal) : Measurable (noncentralFPDFReal m n l)

Measurability of the real density in its argument.

theorem TauCeti.Probability.measurable_noncentralFPDF (m n : ℝ) (l : NNReal) : Measurable (noncentralFPDF m n l)

Measurability of the extended density in its argument.

theorem TauCeti.Probability.noncentralFPDF_eq_tsum {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) (x : ℝ) : noncentralFPDF m n l x = ∑' (j : ℕ), (ProbabilityTheory.poissonMeasure (l / 2)) {j} * ENNReal.ofReal (m / (m + 2 * ↑j)) * fisherSnedecorPDF (m + 2 * ↑j) n (m * x / (m + 2 * ↑j))

The extended density is the Poisson series of scaled central F densities at every point.

theorem TauCeti.Probability.noncentralFMeasure_eq_withDensity (m n : ℝ) (l : NNReal) : noncentralFMeasure m n l = MeasureTheory.volume.withDensity (noncentralFPDF m n l)

The noncentral F ratio law has its Poisson-series density, including invalid degrees.

theorem TauCeti.Probability.lintegral_noncentralFPDF_eq_one {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) : ∫⁻ (x : ℝ), noncentralFPDF m n l x = 1

The extended density integrates to one for positive degrees.

theorem TauCeti.Probability.integrable_noncentralFPDFReal (m n : ℝ) (l : NNReal) : MeasureTheory.Integrable (noncentralFPDFReal m n l) MeasureTheory.volume

The real density is integrable, also at invalid degrees where it vanishes.

theorem TauCeti.Probability.integral_noncentralFPDFReal_eq_one {m n : ℝ} (hm : 0 < m) (hn : 0 < n) (l : NNReal) : ∫ (x : ℝ), noncentralFPDFReal m n l x = 1

The real density integrates to one for positive degrees.

theorem TauCeti.Probability.rnDeriv_noncentralFMeasure (m n : ℝ) (l : NNReal) : (noncentralFMeasure m n l).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] noncentralFPDF m n l

The Radon–Nikodym derivative of the noncentral F law is the named density.

theorem TauCeti.Probability.pdf_eq_noncentralFPDF_of_hasLaw_noncentralFMeasure {m n : ℝ} {l : NNReal} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (noncentralFMeasure m n l) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] noncentralFPDF m n l

The canonical density of a variable with noncentral F law is the named density.