English
If a function f is differentiable on a convex open set s, continuous on its closure and its derivative converges to a limit f′ at a boundary point x, then f is differentiable at x with derivative f′, in the sense of within the closure of s.
Русский
Если функция f дифференцируема на выпуклом открытом множестве s, непрерывна на замкнутом дополнении и производная сходится к пределу f′ в точке границы x, то в точке x функция дифференцируема с производной f′ в смысле внутри замкнутого множества.
LaTeX
$$$$ \\text{If } f \\text{ differentiable on } s, \\text{ convex open}, \\text{ and } f \\text{ continuous on } \\overline{s}, \\text{ with } \\lim_{y\\to x,\, y\\in s} f'(y)=f', \\text{ then } \\exists \\text{ HasFDerivWithinAt } f f' (\\overline{s}) x. $$$$
Lean4
/-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
with derivative `f'`. -/
theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F}
(f_diff : DifferentiableOn ℝ f s) (s_conv : Convex ℝ s) (s_open : IsOpen s)
(f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y) (h : Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) :
HasFDerivWithinAt f f' (closure s) x := by
classical
-- one can assume without loss of generality that `x` belongs to the closure of `s`, as the
-- statement is empty otherwise
by_cases hx : x ∉ closure s
· rw [← closure_closure] at hx; exact HasFDerivWithinAt.of_notMem_closure hx
push_neg at hx
rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleO, Asymptotics.isLittleO_iff]
/- One needs to show that `‖f y - f x - f' (y - x)‖ ≤ ε ‖y - x‖` for `y` close to `x` in
`closure s`, where `ε` is an arbitrary positive constant. By continuity of the functions, it
suffices to prove this for nearby points inside `s`. In a neighborhood of `x`, the derivative
of `f` is arbitrarily close to `f'` by assumption. The mean value inequality completes the
proof. -/
intro ε ε_pos
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε := by
simpa [dist_zero_right] using tendsto_nhdsWithin_nhds.1 h ε ε_pos
set B := ball x δ
suffices ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖ from
mem_nhdsWithin_iff.2 ⟨δ, δ_pos, fun y hy => by simpa using this y hy⟩
suffices ∀ p : E × E, p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
by
rw [closure_prod_eq] at this
intro y y_in
apply this ⟨x, y⟩
have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩
have key : ∀ p : E × E, p ∈ (B ∩ s) ×ˢ (B ∩ s) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖ :=
by
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
have conv : Convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv
have diff : DifferentiableOn ℝ f (B ∩ s) := f_diff.mono inter_subset_right
have bound : ∀ z ∈ B ∩ s, ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε :=
by
intro z z_in
have h := hδ z
have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z :=
by
have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
rw [← this] at h
exact le_of_lt (h z_in.2 z_in.1)
simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in
rintro ⟨u, v⟩ uv_in
have f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y :=
by
intro y y_in
exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt
refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key
all_goals
-- common start for both continuity proofs
have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by gcongr <;> exact inter_subset_right
obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by simpa [closure_prod_eq] using closure_mono this uv_in
apply ContinuousWithinAt.mono _ this
simp only [ContinuousWithinAt]
· rw [nhdsWithin_prod_eq]
have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel
simp only [this]
exact
Tendsto.comp continuous_norm.continuousAt
((Tendsto.comp (f_cont' v v_in) tendsto_snd).sub <| Tendsto.comp (f_cont' u u_in) tendsto_fst)
· apply tendsto_nhdsWithin_of_tendsto_nhds
rw [nhds_prod_eq]
exact tendsto_const_nhds.mul (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)
