English
For a convex f on S, the function x ↦ derivWithin f(Ioi x) x is monotone on interior S.
Русский
Для выпуклой f на S функция x ↦ derivWithin f(Ioi x) x монотонна на interior S.
LaTeX
$$$$ \ MonotoneOn\ (\lambda x.\ derivWithin\ f\ (Ioi\ x)\ x)\ (\operatorname{interior} S) $$$$
Lean4
theorem monotoneOn_rightDeriv (hfc : ConvexOn ℝ S f) : MonotoneOn (fun x ↦ derivWithin f (Ioi x) x) (interior S) :=
by
intro x hxs y hys hxy
rcases eq_or_lt_of_le hxy with rfl | hxy; · rfl
simp_rw [hfc.rightDeriv_eq_sInf_slope_of_mem_interior hxs, hfc.rightDeriv_eq_sInf_slope_of_mem_interior hys]
refine
csInf_le_of_le (b := slope f x y) (bddBelow_slope_lt_of_mem_interior hfc hxs)
⟨y, by simp only [mem_setOf_eq, hxy, and_true]; exact interior_subset hys⟩ (le_csInf ?_ ?_)
· have hys' := hys
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hys'
obtain ⟨a, b, hxab, habs⟩ := hys'
rw [image_nonempty]
obtain ⟨z, hxz, hzb⟩ := exists_between hxab.2
exact ⟨z, habs ⟨hxab.1.trans hxz, hzb⟩, hxz⟩
· rintro _ ⟨z, ⟨hzs, hyz : y < z⟩, rfl⟩
rw [slope_comm]
exact slope_mono hfc (interior_subset hys) ⟨interior_subset hxs, hxy.ne⟩ ⟨hzs, hyz.ne'⟩ (hxy.trans hyz).le
