← Mathematical handbook

theorem Verification.convex_increment_Ioo {f : ℝ → ℝ} {r : ℝ} (hf : ConvexOn ℝ (Set.Ioo 0 r) f) {a b c e : ℝ} (ha : 0 < a) (hc : 0 ≤ c) (hab : a ≤ b) (hce : c ≤ e) (hbr : b + e < r) : 0 ≤ f (b + e) - f (a + e) - f (b + c) + f (a + c)

theorem Verification.n22Prime_ratio_antitone {p : ℝ} (hp : 1 ≤ p) (k : ℝ) (hk : 0 ≤ k) : AntitoneOn (fun (t : ℝ) => n22Prime p (t + k) / n22Prime p t) (Set.Ioo 0 (Real.pi / 2))

theorem Verification.n22Phi_mem {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : Real.arcsin (1 - u ^ θ) ∈ Set.Ioo 0 (Real.pi / 2)

theorem Verification.n22Phi_deriv {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => Real.arcsin (1 - x ^ θ)) (1 / √(1 - (1 - u ^ θ) ^ 2) * -(θ * u ^ (θ - 1))) u

theorem Verification.nelsen22_isCD_positive {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : (nelsen22 θ ⋯).IsCD

theorem Verification.nelsen22_isCD (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (nelsen22 θ hθ).IsCD