← Mathematical handbook

theorem Verification.nelsen13_section_concave (θ : ℝ) (hθ : 1 ≤ θ) (v : ↑unitInterval) : ConcaveOn ℝ (Set.Icc 0 1) ((nelsen13 θ ⋯).cdfSection v)

theorem Verification.nelsen13_isCI (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen13 θ ⋯).IsCI

theorem Verification.nelsen13_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (nelsen13 θ ⋯).SchurBothLE (nelsen13 η ⋯)

theorem Verification.n13_power_comparison_strict (r : ℝ) (hr : 1 < r) {a b : ℝ} (ha : 1 < a) (hb : 1 < b) : a ^ r + b ^ r - 1 < (a + b - 1) ^ r

theorem Verification.nelsen13_not_pqd_below_one (θ : ℝ) (hθ : 0 ≤ θ) (hθ1 : θ < 1) : ¬(nelsen13 θ hθ).IsPQD

theorem Verification.nelsen13_isCI_iff (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen13 θ hθ).IsCI ↔ 1 ≤ θ

theorem Verification.nelsen13_density_tp2_requires_one (θ : ℝ) (hθ : 0 ≤ θ) (hd : (nelsen13 θ hθ).HasMTP2Density) : 1 ≤ θ