English
A refined formulation of HasDerivWithinAt_sInf_slope for an indexed slope image over a subset.
Русский
Уточненная формулировка HasDerivWithinAt_sInf_slope для графа наклонов над подмножеством.
LaTeX
$$$\\forall {α} {β} [Preorder α] {a x},\\; \\text{HasDerivWithinAt f f' a x} \\Leftrightarrow \\, \\text{Tendsto } (\\text{slope } f x) (nhdsWithin x (S \\{x})) (nhds f').$$
Lean4
theorem hasDerivWithinAt_sInf_slope_of_mem_interior (hfc : ConvexOn ℝ S f) (hxs : x ∈ interior S) :
HasDerivWithinAt f (sInf (slope f x '' {y ∈ S | x < y})) (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'
simp_rw [hasDerivWithinAt_iff_tendsto_slope]
simp only [mem_Ioi, lt_self_iff_false, not_false_eq_true, diff_singleton_eq_self]
have h : Ioo x b ⊆ {y | y ∈ S ∧ x < y} := fun z hz ↦ ⟨habs ⟨hxab.1.trans hz.1, hz.2⟩, hz.1⟩
have h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b))) :=
((monotoneOn_slope_gt hfc (habs hxab)).mono h).tendsto_nhdsWithin_Ioo_right (by simpa using hxab.2)
((bddBelow_slope_lt_of_mem_interior hfc hxs).mono (image_mono h))
suffices sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y ∈ S | x < y}) by rwa [← this]
apply
(monotoneOn_slope_gt hfc (habs hxab)).csInf_eq_of_subset_of_forall_exists_le
(bddBelow_slope_lt_of_mem_interior hfc hxs) h ?_
rintro y ⟨hyS, hxy⟩
obtain ⟨z, hxz, hzy⟩ := exists_between (lt_min hxab.2 hxy)
exact ⟨z, ⟨hxz, hzy.trans_le (min_le_left _ _)⟩, hzy.le.trans (min_le_right _ _)⟩
