← Mathematical handbook

theorem Verification.antitone_unit_extension {f : ↑unitInterval → ℝ} (hf : ∀ (u : ↑unitInterval), f u ∈ Set.Icc 0 1) (ha : AntitoneOn f {u : ↑unitInterval | ↑u ∈ Set.Ioo 0 1}) : Antitone fun (u : ↑unitInterval) => if u = 0 then 1 else if u = 1 then 0 else f u

theorem Verification.gaussianBivariate_isSI {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hpos : 0 ≤ r) : (gaussianBivariate r hr).IsSI

theorem Verification.gaussianBivariate_isCI {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hpos : 0 ≤ r) : (gaussianBivariate r hr).IsCI

theorem Verification.gaussianBivariate_isSD {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hneg : r ≤ 0) : (gaussianBivariate r hr).IsSD

theorem Verification.gaussianBivariate_isCD {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hneg : r ≤ 0) : (gaussianBivariate r hr).IsCD

theorem Verification.gaussianBivariate_isPQD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).IsPQD ↔ 0 ≤ r

theorem Verification.gaussianBivariate_isNQD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).IsNQD ↔ r ≤ 0

theorem Verification.gaussianBivariate_isCI_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).IsCI ↔ 0 ≤ r

theorem Verification.gaussianBivariate_isCD_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).IsCD ↔ r ≤ 0