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