← Mathematical handbook

theorem Papers.AnsariRockel2024.student_precision_centered_second_moment (ν : ℝ) (hν : 0 < ν) : MeasureTheory.Integrable (fun (t : ℝ) => (t - 1) ^ 2) (ProbabilityTheory.gammaMeasure (ν / 2) (ν / 2)) ∧ ∫ (t : ℝ), (t - 1) ^ 2 ∂ProbabilityTheory.gammaMeasure (ν / 2) (ν / 2) = 2 / ν

theorem Papers.AnsariRockel2024.student_precision_concentration_bound (ν : ℝ) (hν : 0 < ν) {ε : ℝ} (hε : 0 < ε) : (ProbabilityTheory.gammaMeasure (ν / 2) (ν / 2)).real {t : ℝ | ε ≤ |t - 1|} ≤ 2 / (ν * ε ^ 2)

theorem Papers.AnsariRockel2024.student_precision_concentrates {ι : Type u_1} {l : Filter ι} (ν : ι → ℝ) (hν : ∀ (i : ι), 0 < ν i) (ht : Filter.Tendsto ν l Filter.atTop) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (i : ι) => (ProbabilityTheory.gammaMeasure (ν i / 2) (ν i / 2)).real {t : ℝ | ε ≤ |t - 1|}) l (nhds 0)

Concentration of the actual Student gamma precision; the copula limit requires additional marginal and joint CDF arguments.