← Mathematical handbook

theorem Verification.n16Inv_deriv_pos {θ u : ℝ} (hu : 0 < u) : HasDerivAt (n16Inv θ) (-n16Weight θ u) u

theorem Verification.n16RealCDF_deriv_pos {θ u v : ℝ} (hθ : 0 < θ) (hu : 0 < u) : HasDerivAt (fun (x : ℝ) => n16RealCDF θ x v) (n16Partial θ u v) u

theorem Verification.n16Weight_deriv {θ u : ℝ} (hu : 0 < u) : HasDerivAt (n16Weight θ) (-2 * θ / u ^ 3) u

theorem Verification.n16Partial_deriv_left {θ u v : ℝ} (hθ : 0 < θ) (hu : 0 < u) : HasDerivAt (fun (x : ℝ) => n16Partial θ x v) (n16Second θ (n16Inv θ u + n16Inv θ v) * n16Weight θ u ^ 2 + n16PsiDeriv θ (n16Inv θ u + n16Inv θ v) * (2 * θ / u ^ 3)) u

theorem Verification.n16RealCDF_eq {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : n16RealCDF θ ↑u ↑v = (nelsen16 θ ⋯).cdf ![u, v]

theorem Verification.n16_curvature_nonpos_of_isSI {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).IsSI) (v : ↑unitInterval) (hv : 0 < ↑v) : n16Second θ (n16Inv θ ↑v) * (1 + θ) ^ 2 + n16PsiDeriv θ (n16Inv θ ↑v) * (2 * θ) ≤ 0

theorem Verification.n16Rad_inv {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) (hv : 0 < ↑v) : n16Rad θ (n16Inv θ ↑v) = ↑v + θ / ↑v

theorem Verification.n16_boundary_polynomial_nonpos {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).IsSI) (v : ↑unitInterval) (hv : 0 < ↑v) : ↑v * (1 + θ) ^ 2 - (↑v ^ 2 + θ) ^ 2 ≤ 0

theorem Verification.nelsen16_ci_requires_three_pos {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).IsCI) : 3 ≤ θ

theorem Verification.nelsen16_ci_iff (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).IsCI ↔ 3 ≤ θ