← Mathematical handbook

noncomputable def Verification.n11ComparisonBase (t : ℝ) : ℝ

Equations

• Verification.n11ComparisonBase t = 2 - Real.exp t

noncomputable def Verification.n11Comparison (r t : ℝ) : ℝ

Equations

• Verification.n11Comparison r t = Real.log (2 - Verification.n11ComparisonBase t ^ r)

noncomputable def Verification.n11ComparisonDeriv (r t : ℝ) : ℝ

Equations

• Verification.n11ComparisonDeriv r t = r * Real.exp t * Verification.n11ComparisonBase t ^ r / (Verification.n11ComparisonBase t * (2 - Verification.n11ComparisonBase t ^ r))

theorem Verification.n11Comparison_deriv (r t : ℝ) (ha : 0 < n11ComparisonBase t) (hd : 2 - n11ComparisonBase t ^ r ≠ 0) : HasDerivAt (n11Comparison r) (n11ComparisonDeriv r t) t

theorem Verification.n11Comparison_deriv2 (r t : ℝ) (ha : 0 < n11ComparisonBase t) (hd : 2 - n11ComparisonBase t ^ r ≠ 0) : HasDerivAt (n11ComparisonDeriv r) (2 * r * Real.exp t * n11ComparisonBase t ^ r * (r * n11ComparisonBase t - 2 * r + 2 - n11ComparisonBase t ^ r) / (n11ComparisonBase t ^ 2 * (2 - n11ComparisonBase t ^ r) ^ 2)) t

theorem Verification.n11Comparison_concave (r : ℝ) (hr : 1 ≤ r) : ConcaveOn ℝ (Set.Icc 0 (Real.log 2)) (n11Comparison r)

theorem Verification.n11Comparison_subadd (r : ℝ) (hr : 1 ≤ r) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t ≤ Real.log 2) : n11Comparison r (s + t) ≤ n11Comparison r s + n11Comparison r t

theorem Verification.n11_power_comparison (r : ℝ) (hr : 1 ≤ r) {a b : ℝ} (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) : max 0 (2 - (2 - a ^ r) * (2 - b ^ r)) ≤ max 0 (2 - (2 - a) * (2 - b)) ^ r