Theorems · Theorem · real analysis

hasFDerivWithinAt_closure_of_tendsto_fderiv

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {f' : E →L[ℝ] F},
  DifferentiableOn ℝ f s →
    Convex ℝ s →
      IsOpen s →
        (∀ y ∈ closure s, ContinuousWithinAt f s y) →
          Filter.Tendsto (fun y => 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'.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Extend

Cited by

2 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace