Extending differentiability to the boundary

We investigate how differentiable functions inside a set extend to differentiable functions on the boundary. For this, it suffices that the function and its derivative admit limits there. A general version of this statement is given in hasFDerivWithinAt_closure_of_tendsto_fderiv.

One-dimensional versions, in which one wants to obtain differentiability at the left endpoint or the right endpoint of an interval, are given in hasDerivWithinAt_Ici_of_tendsto_deriv and hasDerivWithinAt_Iic_of_tendsto_deriv. These versions are formulated in terms of the one-dimensional derivative deriv ℝ f.

theorem hasFDerivWithinAt_closure_of_tendsto_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {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 : Filter.Tendsto (fun (y : E) => fderiv ℝ f y) (nhdsWithin x s) (nhds f')) : HasFDerivWithinAt f f' (closure s) x

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'.

@[deprecated hasFDerivWithinAt_closure_of_tendsto_fderiv]

theorem has_fderiv_at_boundary_of_tendsto_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {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 : Filter.Tendsto (fun (y : E) => fderiv ℝ f y) (nhdsWithin x s) (nhds f')) : HasFDerivWithinAt f f' (closure s) x

Alias of hasFDerivWithinAt_closure_of_tendsto_fderiv.

---

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 hasDerivWithinAt_Ici_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E} (f_diff : DifferentiableOn ℝ f s) (f_lim : ContinuousWithinAt f s a) (hs : s ∈ nhdsWithin a (Set.Ioi a)) (f_lim' : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds e)) : HasDerivWithinAt f e (Set.Ici a) a

If a function is differentiable on the right of a point a : ℝ, continuous at a, and its derivative also converges at a, then f is differentiable on the right at a.

@[deprecated hasDerivWithinAt_Ici_of_tendsto_deriv]

theorem has_deriv_at_interval_left_endpoint_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E} (f_diff : DifferentiableOn ℝ f s) (f_lim : ContinuousWithinAt f s a) (hs : s ∈ nhdsWithin a (Set.Ioi a)) (f_lim' : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds e)) : HasDerivWithinAt f e (Set.Ici a) a

Alias of hasDerivWithinAt_Ici_of_tendsto_deriv.

---

If a function is differentiable on the right of a point a : ℝ, continuous at a, and its derivative also converges at a, then f is differentiable on the right at a.

theorem hasDerivWithinAt_Iic_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E} (f_diff : DifferentiableOn ℝ f s) (f_lim : ContinuousWithinAt f s a) (hs : s ∈ nhdsWithin a (Set.Iio a)) (f_lim' : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin a (Set.Iio a)) (nhds e)) : HasDerivWithinAt f e (Set.Iic a) a

If a function is differentiable on the left of a point a : ℝ, continuous at a, and its derivative also converges at a, then f is differentiable on the left at a.

@[deprecated hasDerivWithinAt_Iic_of_tendsto_deriv]

theorem has_deriv_at_interval_right_endpoint_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E} (f_diff : DifferentiableOn ℝ f s) (f_lim : ContinuousWithinAt f s a) (hs : s ∈ nhdsWithin a (Set.Iio a)) (f_lim' : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin a (Set.Iio a)) (nhds e)) : HasDerivWithinAt f e (Set.Iic a) a

Alias of hasDerivWithinAt_Iic_of_tendsto_deriv.

---

If a function is differentiable on the left of a point a : ℝ, continuous at a, and its derivative also converges at a, then f is differentiable on the left at a.

theorem hasDerivAt_of_hasDerivAt_of_ne {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ} (f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) (hf : ContinuousAt f x) (hg : ContinuousAt g x) : HasDerivAt f (g x) x

If a real function f has a derivative g everywhere but at a point, and f and g are continuous at this point, then g is also the derivative of f at this point.

theorem hasDerivAt_of_hasDerivAt_of_ne' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {x : ℝ} (f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y) (hf : ContinuousAt f x) (hg : ContinuousAt g x) (y : ℝ) : HasDerivAt f (g y) y

If a real function f has a derivative g everywhere but at a point, and f and g are continuous at this point, then g is the derivative of f everywhere.