Mean_Value_of_Convex_Real_Function
Provedanalysisconvex-functionsmean-valueproofwiki
If f is convex, continuous on [a,b] and differentiable on (a,b), then f(x) lies below the secant line for x in (a,b).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Mean_Value_of_Convex_Real_Function (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (hfconv : ConvexOn ℝ (Set.Ioo a b) f) (x : ℝ) (hx : x ∈ Set.Ioo a b) : f x ≤ f a + (f b - f a) / (b - a) * (x - a) := by sorry
Source