← Mathematical handbook

theorem Verification.antitone_of_continuous_ae_eq {f g : ℝ → ℝ} (hf : Continuous f) (hg : Antitone g) (he : f =ᵐ[MeasureTheory.volume] g) : Antitone f

noncomputable def Verification.studentConditionalScore (r ν b x : ℝ) : ℝ

Equations

• Verification.studentConditionalScore r ν b x = (b - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1))

theorem Verification.continuous_studentConditionalScore {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {ν : ℝ} (hν : 0 < ν) (b : ℝ) : Continuous (studentConditionalScore r ν b)

theorem Verification.studentConditionalScore_not_antitone {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) {ν : ℝ} (hν : 0 < ν) : ¬Antitone (studentConditionalScore r ν (3 * √ν))

theorem Verification.studentBivariate_not_isSI {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : ¬(studentBivariate r ⋯ ν hν).IsSI

theorem Verification.studentBivariate_not_isCI {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : ¬(studentBivariate r ⋯ ν hν).IsCI

theorem Verification.studentBivariate_not_isSD {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : ¬(studentBivariate r ⋯ ν hν).IsSD

theorem Verification.studentBivariate_not_isCD {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : ¬(studentBivariate r ⋯ ν hν).IsCD

theorem Verification.studentBivariate_isSI_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).IsSI ↔ r = 1

theorem Verification.studentBivariate_isCI_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).IsCI ↔ r = 1

theorem Verification.studentBivariate_isSD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).IsSD ↔ r = -1

theorem Verification.studentBivariate_isCD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).IsCD ↔ r = -1

theorem Verification.studentBivariate_not_hasMTP2Density {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : ¬(studentBivariate r hr ν hν).HasMTP2Density