← Mathematical handbook

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

Equations

• Verification.joeComparisonBase t = 1 - Real.exp (-t)

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

Equations

• Verification.joeComparison r t = -Real.log (1 - Verification.joeComparisonBase t ^ r)

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

Equations

• Verification.joeComparisonDeriv r t = r * Real.exp (-t) * Verification.joeComparisonBase t ^ r / (Verification.joeComparisonBase t * (1 - Verification.joeComparisonBase t ^ r))

theorem Verification.joeComparison_deriv (r t : ℝ) (ha : 0 < joeComparisonBase t) (hd : 1 - joeComparisonBase t ^ r ≠ 0) : HasDerivAt (joeComparison r) (joeComparisonDeriv r t) t

theorem Verification.joeComparison_deriv2 (r t : ℝ) (ha : 0 < joeComparisonBase t) (hd : 1 - joeComparisonBase t ^ r ≠ 0) : HasDerivAt (joeComparisonDeriv r) (r * Real.exp (-t) * joeComparisonBase t ^ r * (r * Real.exp (-t) - 1 + joeComparisonBase t ^ r) / (joeComparisonBase t ^ 2 * (1 - joeComparisonBase t ^ r) ^ 2)) t

theorem Verification.joeComparison_convex (r : ℝ) (hr : 1 ≤ r) : ConvexOn ℝ (Set.Ici 0) (joeComparison r)

theorem Verification.joeComparison_superadd (r : ℝ) (hr : 1 ≤ r) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : joeComparison r s + joeComparison r t ≤ joeComparison r (s + t)

theorem Verification.joe_power_comparison (r : ℝ) (hr : 1 ≤ r) {a b : ℝ} (ha : a ∈ Set.Ico 0 1) (hb : b ∈ Set.Ico 0 1) : a ^ r + b ^ r - a ^ r * b ^ r ≤ (a + b - a * b) ^ r