English
For a convex set and interior point, HasDerivWithinAt equals slope supremum construction.
Русский
Для выпуклого множества и внутренней точки HasDerivWithinAt равен верхушке наклонов.
LaTeX
$$$\\forall S f x,\\; \\text{ConvexOn } \\mathbb{R} \\, S \\, f \\Rightarrow \\text{HasDerivWithinAt } f (\\text{sup of slopes}) (Iio x) x.$$
Lean4
theorem hasDerivWithinAt_sSup_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (sSup (slope f x '' {y ∈ S | y < x})) (Iio 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'
simp_rw [hasDerivWithinAt_iff_tendsto_slope]
simp only [mem_Iio, lt_self_iff_false, not_false_eq_true, diff_singleton_eq_self]
have h : Ioo a x ⊆ {y | y ∈ S ∧ y < x} := fun z hz ↦ ⟨habs ⟨hz.1, hz.2.trans hxab.2⟩, hz.2⟩
have h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x))) :=
((monotoneOn_slope_lt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_left (by simpa using hxab.1)
((bddAbove_slope_gt_of_mem_interior hfc hxs).mono (image_mono h))
suffices sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y ∈ S | y < x}) by rwa [← this]
apply
(monotoneOn_slope_lt hfc (habs hxab)).csSup_eq_of_subset_of_forall_exists_le
(bddAbove_slope_gt_of_mem_interior hfc hxs) h ?_
rintro y ⟨hyS, hyx⟩
obtain ⟨z, hyz, hzx⟩ := exists_between (max_lt hxab.1 hyx)
exact ⟨z, ⟨(le_max_left _ _).trans_lt hyz, hzx⟩, (le_max_right _ _).trans hyz.le⟩
