Parameter measurability of Fisher's F distribution

This file proves that the Fisher--Snedecor law is a measurable function of its two degrees of freedom. Consequently, measurable numerator and denominator parameters can be used to form a probability kernel whenever they lie in the positive range.

Joint measurability of the density is exposed alongside the measure-level result, so both the law and its density can be composed with measurable parameter maps.

Main results

• measurable_uncurry_fisherSnedecorPDF — joint measurability of the density.
• measurable_fisherSnedecorMeasure — joint parameter measurability of the family of measures.

theorem TauCeti.Probability.measurable_uncurry_fisherSnedecorPDF : Measurable fun (q : (ℝ × ℝ) × ℝ) => fisherSnedecorPDF q.1.1 q.1.2 q.2

The Fisher--Snedecor density is jointly measurable in the numerator and denominator degrees of freedom and the sample point.

theorem TauCeti.Probability.measurable_fisherSnedecorMeasure : Measurable fun (p : ℝ × ℝ) => fisherSnedecorMeasure p.1 p.2

The Fisher--Snedecor family is jointly measurable in its two degrees of freedom.

This theorem includes every invalid parameter pair, where fisherSnedecorMeasure is the zero measure.