English
The left slope is bounded above by the left-derivative within the left interval.
Русский
Левый наклон ограничен левой производной на отрезке слева от x.
LaTeX
$$$$ \ slope\ f x y \le \ derivWithin\ f( Iio y ) y $$$$
Lean4
/-- If `f : ℝ → ℝ` is convex on `S` and left-differentiable at `y ∈ S`, then the slope of any secant
line with right endpoint at `y` is bounded above by the left derivative of `f` at `y`. -/
theorem slope_le_of_hasDerivWithinAt_Iio (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
(hf' : HasDerivWithinAt f f' (Iio y) y) : slope f x y ≤ f' :=
by
apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' notMem_Iio_self).mp hf'
simp_rw [eventually_nhdsWithin_iff, slope_comm f x y, slope_def_field]
filter_upwards [eventually_gt_nhds hxy] with t ht (ht' : t < y)
refine hfc.secant_mono hy hx (?_ : t ∈ S) hxy.ne ht'.ne ht.le
exact hfc.1.ordConnected.out hx hy ⟨ht.le, ht'.le⟩
