← Mathematical handbook

theorem Verification.student_diagonal_score_negative {r ν x : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hν : 0 < ν) (hx : x < 0) : studentConditionalScore r ν x x = -(1 - r) / √((1 + ν * x⁻¹ ^ 2) * (1 - r ^ 2) / (ν + 1))

theorem Verification.student_diagonal_score_tendsto {r ν : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hν : 0 < ν) : Filter.Tendsto (fun (x : ℝ) => studentConditionalScore r ν x x) Filter.atBot (nhds (-(1 - r) / √((1 - r ^ 2) / (ν + 1))))