Differentiable_Bounded_Convex_is_Constant
Provedanalysisbounded-functionsconvex-functionsproofwiki
A differentiable, bounded, convex function on R is constant.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
theorem Differentiable_Bounded_Convex_is_Constant (f : ℝ → ℝ) (hd : Differentiable ℝ f) (hb : ∃ M, ∀ x, |f x| ≤ M) (hc : ConvexOn ℝ Set.univ f) : ∃ c : ℝ, ∀ x, f x = c := by sorry
Source