Eventual differentiability of C^n maps

Because ContDiffWithinAt 𝕜 1 f s x propagates to a 𝓝[insert x s] x-neighborhood (ContDiffWithinAt.eventually) and implies DifferentiableWithinAt, any map that is C^n at (or within s at) x with 1 ≤ n is differentiable near x. Lowering to order 1 first avoids the n ≠ ∞ restriction of ContDiffAt.eventually, so both n = ∞ and n = ω are covered.

Main declarations

• ContDiffWithinAt.eventually_differentiableWithinAt: C^n within s at x (1 ≤ n) implies DifferentiableWithinAt eventually in 𝓝[insert x s] x.
• ContDiffAt.eventually_differentiableAt: C^n at x (1 ≤ n) implies DifferentiableAt eventually in 𝓝 x.
• ContDiffAt.differentiableAt_deriv_two: the derivative of a function of one variable that is C² at x is differentiable at x.

theorem ContDiffWithinAt.eventually_differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} {s : Set E} {x : E} (hf : ContDiffWithinAt 𝕜 n f s x) (hn : 1 ≤ n) : ∀ᶠ (y : E) in nhdsWithin x (insert x s), DifferentiableWithinAt 𝕜 f s y

If f is C^n within s at x with 1 ≤ n, then f is differentiable within s at all points in a 𝓝[insert x s] x-neighborhood of x.

theorem ContDiffAt.eventually_differentiableAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : E → F} {x : E} (hf : ContDiffAt 𝕜 n f x) (hn : 1 ≤ n) : ∀ᶠ (y : E) in nhds x, DifferentiableAt 𝕜 f y

If f is C^n at x with 1 ≤ n, then f is differentiable on a neighborhood of x.

theorem ContDiffAt.differentiableAt_deriv_two {𝕜 : Type u_1} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (hf : ContDiffAt 𝕜 2 f x) : DifferentiableAt 𝕜 (deriv f) x

The derivative of a function of one variable that is C² at x is differentiable at x.