English
For a convex f on interior of S, the left derivative at x is not larger than the right derivative at x.
Русский
Для выпуклой f на interior S левый производной в x не больше правого производного в x.
LaTeX
$$$$ \ derivWithin\ f(Iio x) x \le \ derivWithin\ f(Ioi x) x $$$$
Lean4
theorem leftDeriv_le_rightDeriv_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x :=
by
have hxs' := hxs
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hxs'
obtain ⟨a, b, hxab, habs⟩ := hxs'
rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs, hfc.leftDeriv_eq_sSup_slope_of_mem_interior hxs]
refine csSup_le ?_ ?_
· rw [image_nonempty]
obtain ⟨z, haz, hzx⟩ := exists_between hxab.1
exact ⟨z, habs ⟨haz, hzx.trans hxab.2⟩, hzx⟩
rintro _ ⟨z, ⟨hzs, hzx⟩, rfl⟩
refine le_csInf ?_ ?_
· rw [image_nonempty]
obtain ⟨z, hxz, hzb⟩ := exists_between hxab.2
exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩
rintro _ ⟨y, ⟨hys, hxy⟩, rfl⟩
exact slope_mono hfc (interior_subset hxs) ⟨hzs, hzx.ne⟩ ⟨hys, hxy.ne'⟩ (hzx.trans hxy).le
