English
If f is convex on S, x<y in S, and f' is a derivative within Ioi x, then f' ≤ slope f x y.
Русский
Пусть f выпукла на S, x<y и f имеет производную внутри Ioi x; тогда f' ≤ slope f x y.
LaTeX
$$$$ f' \le \operatorname{slope}(f,x,y) $$$$
Lean4
/-- If `f : ℝ → ℝ` is convex on `S` and right-differentiable at `x ∈ S`, then the slope of any
secant line with left endpoint at `x` is bounded below by the right derivative of `f` at `x`. -/
theorem le_slope_of_hasDerivWithinAt_Ioi (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hf' : HasDerivWithinAt f f' (Ioi x) x) : f' ≤ slope f x y :=
by
apply le_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' notMem_Ioi_self).mp hf'
simp_rw [eventually_nhdsWithin_iff, slope_def_field]
filter_upwards [eventually_lt_nhds hxy] with t ht (ht' : x < t)
refine hfc.secant_mono hx (?_ : t ∈ S) hy ht'.ne' hxy.ne' ht.le
exact hfc.1.ordConnected.out hx hy ⟨ht'.le, ht.le⟩
