← Mathematical handbook

noncomputable def Verification.n17Comparison (a b t : ℝ) : ℝ

Equations

• Verification.n17Comparison a b t = -Real.log ((Verification.n17Base a t ^ (b / a) - 1) / Verification.n17A b)

noncomputable def Verification.n17ComparisonPrime (a b t : ℝ) : ℝ

Equations

• Verification.n17ComparisonPrime a b t = b / a * Verification.n17A a * Real.exp (-t) * Verification.n17Base a t ^ (b / a - 1) / (Verification.n17Base a t ^ (b / a) - 1)

theorem Verification.n17Comparison_denom {a b t : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (ht : 0 ≤ t) : n17Base a t ^ (b / a) - 1 ≠ 0

theorem Verification.n17Comparison_deriv {a b t : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (ht : 0 ≤ t) : HasDerivAt (n17Comparison a b) (n17ComparisonPrime a b t) t

theorem Verification.n17Comparison_deriv2 {a b t : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (ht : 0 ≤ t) : HasDerivAt (n17ComparisonPrime a b) (b / a * n17A a * Real.exp (-t) * n17Base a t ^ (b / a - 2) * (1 + b / a * n17A a * Real.exp (-t) - n17Base a t ^ (b / a)) / (n17Base a t ^ (b / a) - 1) ^ 2) t

theorem Verification.n17_bernoulli_nonpos {r q : ℝ} (hr : r ≤ 0) (hq : 0 < 1 + q) : 1 + r * q ≤ (1 + q) ^ r

theorem Verification.n17Comparison_convex {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (hba : b ≤ a) : ConvexOn ℝ (Set.Ici 0) (n17Comparison a b)

theorem Verification.n17Comparison_zero {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) : n17Comparison a b 0 = 0

theorem Verification.n17Comparison_superadd {a b s t : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (hba : b ≤ a) (hs : 0 ≤ s) (ht : 0 ≤ t) : n17Comparison a b s + n17Comparison a b t ≤ n17Comparison a b (s + t)

theorem Verification.n17Comparison_inv {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (u : ↑unitInterval) (hu : u ≠ 0) : n17Comparison a b ((n17Generator a ha).invFun u) = (n17Generator b hb).invFun u

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

theorem Verification.n17Comparison_psi {a b t : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (ht : 0 ≤ t) : n17Psi b (n17Comparison a b t) = n17Psi a t