Student's t and Snedecor's F distributions

TheoremStudent's t law#✓fully proved

Student's t law (Casella–Berger, Definition 5.3.4): for independent Z ~ N(0, 1) and V ~ χ²_k with k ≥ 1, Z / √(V / k) has density Γ((k + 1)/2) / (√(k π) Γ(k/2)) · (1 + t²/k)^{-(k+1)/2}.

theorem map_div_sqrt_chiSquare_eq_studentT {Ω : Type*} [MeasurableSpace Ω]
    {P : Measure Ω} [IsProbabilityMeasure P] {k : ℕ} (hk : 0 < k) {Z V : Ω → ℝ}
    (hZ : HasLaw Z (gaussianReal 0 1) P) (hV : HasLaw V (chiSquareMeasure k) P)
    (hZV : IndepFun Z V P) :
    P.map (fun ω => Z ω / √(V ω / k)) = studentTMeasure k

Uses 1

Statement usesChi-square distribution

• Snedecor's F law
• One-sample t statistic

TheoremHoeffding's central limit theorem#●ready to prove

Hoeffding's central limit theorem (1948, §7): for an i.i.d. sample from μ and a symmetric square-integrable kernel h of degree m, √n (U_n - θ) converges in distribution to N(0, m² σ₁²), where θ = E h and σ₁² = Var h₁.

public theorem_wanted tendstoInDistribution_uStatistic {α : Type*} [MeasurableSpace α]
    (μ : Measure α) [IsProbabilityMeasure μ] {m : ℕ} {h : (Fin m → α) → ℝ}
    (hsymm : ∀ (σ : Equiv.Perm (Fin m)) y, h (y ∘ σ) = h y)
    (hh : MemLp h 2 (Measure.pi fun _ => μ)) :
    TendstoInDistribution
      (fun (n : ℕ) (x : Fin n → α) =>
        √n * (uStatistic h x - ∫ y, h y ∂(Measure.pi fun _ => μ)))
      Filter.atTop id (fun n => Measure.pi fun _ : Fin n => μ)
      (gaussianReal 0
        ((m : ℝ) ^ 2 * Var[hoeffdingProj μ h 1; Measure.pi fun _ : Fin 1 => μ]).toNNReal)

Uses 2

Statement usesHoeffding projection of a kernel · U-statistic

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.