← Mathematical handbook

Convexity from comparisons at geometrically spaced points

theorem Verification.geometric_jensen_chord {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ioi 0)) (hj : ∀ (x r : ℝ), 0 < x → 1 < r → (r + 1) * f x ≤ r * f (x / r) + f (r * x)) {a b c : ℝ} (ha : 0 < a) (hab : a < b) (hbc : b < c) : f b ≤ f a + (b - a) / (c - a) * (f c - f a)

theorem Verification.convexOn_Ioi_of_geometric_jensen {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Ioi 0)) (hj : ∀ (x r : ℝ), 0 < x → 1 < r → (r + 1) * f x ≤ r * f (x / r) + f (r * x)) : ConvexOn ℝ (Set.Ioi 0) f