mathlib3 documentation

analysis.calculus.extend_deriv

Extending differentiability to the boundary #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_fderiv_at_boundary_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 has_deriv_at_interval_left_endpoint_of_tendsto_deriv and has_deriv_at_interval_right_endpoint_of_tendsto_deriv. These versions are formulated in terms of the one-dimensional derivative deriv ℝ f.

theorem has_fderiv_at_boundary_of_tendsto_fderiv {E : Type u_1} [normed_add_comm_group E] [normed_space E] {F : Type u_2} [normed_add_comm_group F] [normed_space F] {f : E F} {s : set E} {x : E} {f' : E →L[] F} (f_diff : differentiable_on f s) (s_conv : convex s) (s_open : is_open s) (f_cont : (y : E), y closure s continuous_within_at f s y) (h : filter.tendsto (λ (y : E), fderiv f y) (nhds_within x s) (nhds f')) :

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 has_deriv_at_interval_left_endpoint_of_tendsto_deriv {E : Type u_1} [normed_add_comm_group E] [normed_space E] {s : set } {e : E} {a : } {f : E} (f_diff : differentiable_on f s) (f_lim : continuous_within_at f s a) (hs : s nhds_within a (set.Ioi a)) (f_lim' : filter.tendsto (λ (x : ), deriv f x) (nhds_within a (set.Ioi a)) (nhds e)) :

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 has_deriv_at_interval_right_endpoint_of_tendsto_deriv {E : Type u_1} [normed_add_comm_group E] [normed_space E] {s : set } {e : E} {a : } {f : E} (f_diff : differentiable_on f s) (f_lim : continuous_within_at f s a) (hs : s nhds_within a (set.Iio a)) (f_lim' : filter.tendsto (λ (x : ), deriv f x) (nhds_within a (set.Iio a)) (nhds e)) :

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 has_deriv_at_of_has_deriv_at_of_ne {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} {x : } (f_diff : (y : ), y x has_deriv_at f (g y) y) (hf : continuous_at f x) (hg : continuous_at g x) :
has_deriv_at 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 has_deriv_at_of_has_deriv_at_of_ne' {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} {x : } (f_diff : (y : ), y x has_deriv_at f (g y) y) (hf : continuous_at f x) (hg : continuous_at g x) (y : ) :
has_deriv_at 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.