← Mathematical handbook

theorem Verification.n16Psi_pos {θ t : ℝ} (hθ : 0 < θ) : 0 < n16Psi θ t

theorem Verification.n16PsiDeriv_eq {θ t : ℝ} (hθ : 0 < θ) : n16PsiDeriv θ t = -n16Psi θ t / n16Rad θ t

theorem Verification.n16PsiDeriv_neg {θ t : ℝ} (hθ : 0 < θ) : n16PsiDeriv θ t < 0

noncomputable def Verification.n16LogDeriv (θ t : ℝ) : ℝ

Equations

• Verification.n16LogDeriv θ t = Real.log (Verification.n16Psi θ t) - Real.log (Verification.n16Rad θ t)

noncomputable def Verification.n16LogDerivPrime (θ t : ℝ) : ℝ

Equations

• Verification.n16LogDerivPrime θ t = (1 - t - θ) / Verification.n16Rad θ t ^ 2 - 1 / Verification.n16Rad θ t

theorem Verification.n16LogDeriv_deriv {θ t : ℝ} (hθ : 0 < θ) : HasDerivAt (n16LogDeriv θ) (n16LogDerivPrime θ t) t

theorem Verification.n16LogDeriv_deriv2 {θ t : ℝ} (hθ : 0 < θ) : HasDerivAt (n16LogDerivPrime θ) (((1 - t - θ) ^ 2 - (1 - t - θ) * n16Rad θ t - 4 * θ) / n16Rad θ t ^ 4) t

theorem Verification.n16LogDeriv_convex {θ : ℝ} (hθ : 3 ≤ θ) : ConvexOn ℝ (Set.Ioi 0) (n16LogDeriv θ)

theorem Verification.n16PsiDeriv_logconvex {θ : ℝ} (hθ : 3 ≤ θ) : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-n16PsiDeriv θ t)

theorem Verification.nelsen16_isCI {θ : ℝ} (hθ : 3 ≤ θ) : (nelsen16 θ ⋯).IsCI

theorem Verification.nelsen16_schur_monotone {θ η : ℝ} (hθ : 3 ≤ θ) (hη : 3 ≤ η) (hθη : θ ≤ η) : (nelsen16 θ ⋯).SchurBothLE (nelsen16 η ⋯)