← Mathematical handbook

Analytic core for Nelsen 17. The auxiliary parameter a is the negative of the paper's parameter, so the power is a⁻¹ on both sign branches.

noncomputable def Verification.n17A (a : ℝ) : ℝ

Equations

• Verification.n17A a = 2 ^ a - 1

noncomputable def Verification.n17Base (a t : ℝ) : ℝ

Equations

• Verification.n17Base a t = 1 + Verification.n17A a * Real.exp (-t)

noncomputable def Verification.n17Psi (a t : ℝ) : ℝ

Equations

• Verification.n17Psi a t = Verification.n17Base a t ^ a⁻¹ - 1

noncomputable def Verification.n17PsiDeriv (a t : ℝ) : ℝ

Equations

• Verification.n17PsiDeriv a t = -a⁻¹ * Verification.n17A a * Real.exp (-t) * Verification.n17Base a t ^ (a⁻¹ - 1)

noncomputable def Verification.n17Second (a t : ℝ) : ℝ

Equations

• Verification.n17Second a t = a⁻¹ * Verification.n17A a * Real.exp (-t) * Verification.n17Base a t ^ (a⁻¹ - 2) * (1 + a⁻¹ * Verification.n17A a * Real.exp (-t))

theorem Verification.n17A_pos {a : ℝ} (ha : 0 < a) : 0 < n17A a

theorem Verification.n17A_neg {a : ℝ} (ha : a < 0) : n17A a < 0

theorem Verification.n17A_ne {a : ℝ} (ha : a ≠ 0) : n17A a ≠ 0

theorem Verification.n17_coeff_pos {a : ℝ} (ha : a ≠ 0) : 0 < a⁻¹ * n17A a

theorem Verification.n17Base_pos {a t : ℝ} (ht : 0 ≤ t) : 0 < n17Base a t

theorem Verification.n17Base_deriv (a t : ℝ) : HasDerivAt (n17Base a) (-n17A a * Real.exp (-t)) t

theorem Verification.n17Psi_deriv {a t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n17Psi a) (n17PsiDeriv a t) t

theorem Verification.n17Psi_deriv2 {a t : ℝ} (ht : 0 ≤ t) : HasDerivAt (n17PsiDeriv a) (n17Second a t) t

theorem Verification.n17Psi_nonneg {a t : ℝ} (ha : a ≠ 0) (ht : 0 ≤ t) : 0 ≤ n17Psi a t

theorem Verification.n17PsiDeriv_neg {a t : ℝ} (ha : a ≠ 0) (ht : 0 ≤ t) : n17PsiDeriv a t < 0

theorem Verification.n17Second_pos {a t : ℝ} (ha : a ≠ 0) (ht : 0 ≤ t) : 0 < n17Second a t

theorem Verification.n17Psi_antitone {a : ℝ} (ha : a ≠ 0) : AntitoneOn (n17Psi a) (Set.Ici 0)

theorem Verification.n17Psi_convex {a : ℝ} (ha : a ≠ 0) : ConvexOn ℝ (Set.Ici 0) (n17Psi a)