doc-next-gen

Mathlib.Analysis.Calculus.ContDiff.Defs

Module docstring

{"# Higher differentiability

A function is C^1 on a domain if it is differentiable there, and its derivative is continuous. By induction, it is C^n if it is C^{n-1} and its (n-1)-th derivative is C^1 there or, equivalently, if it is C^1 and its derivative is C^{n-1}. It is C^∞ if it is C^n for all n. Finally, it is C^Ο‰ if it is analytic (as well as all its derivative, which is automatic if the space is complete).

We formalize these notions with predicates ContDiffWithinAt, ContDiffAt, ContDiffOn and ContDiff saying that the function is C^n within a set at a point, at a point, on a set and on the whole space respectively.

To avoid the issue of choice when choosing a derivative in sets where the derivative is not necessarily unique, ContDiffOn is not defined directly in terms of the regularity of the specific choice iteratedFDerivWithin π•œ n f s inside s, but in terms of the existence of a nice sequence of derivatives, expressed with a predicate HasFTaylorSeriesUpToOn defined in the file FTaylorSeries.

We prove basic properties of these notions.

Main definitions and results

Let f : E β†’ F be a map between normed vector spaces over a nontrivially normed field π•œ.

  • ContDiff π•œ n f: expresses that f is C^n, i.e., it admits a Taylor series up to rank n.
  • ContDiffOn π•œ n f s: expresses that f is C^n in s.
  • ContDiffAt π•œ n f x: expresses that f is C^n around x.
  • ContDiffWithinAt π•œ n f s x: expresses that f is C^n around x within the set s.

In sets of unique differentiability, ContDiffOn π•œ n f s can be expressed in terms of the properties of iteratedFDerivWithin π•œ m f s for m ≀ n. In the whole space, ContDiff π•œ n f can be expressed in terms of the properties of iteratedFDeriv π•œ m f for m ≀ n.

Implementation notes

The definitions in this file are designed to work on any field π•œ. They are sometimes slightly more complicated than the naive definitions one would guess from the intuition over the real or complex numbers, but they are designed to circumvent the lack of gluing properties and partitions of unity in general. In the usual situations, they coincide with the usual definitions.

Definition of C^n functions in domains

One could define C^n functions in a domain s by fixing an arbitrary choice of derivatives (this is what we do with iteratedFDerivWithin) and requiring that all these derivatives up to n are continuous. If the derivative is not unique, this could lead to strange behavior like two C^n functions f and g on s whose sum is not C^n. A better definition is thus to say that a function is C^n inside s if it admits a sequence of derivatives up to n inside s.

This definition still has the problem that a function which is locally C^n would not need to be C^n, as different choices of sequences of derivatives around different points might possibly not be glued together to give a globally defined sequence of derivatives. (Note that this issue can not happen over reals, thanks to partition of unity, but the behavior over a general field is not so clear, and we want a definition for general fields). Also, there are locality problems for the order parameter: one could image a function which, for each n, has a nice sequence of derivatives up to order n, but they do not coincide for varying n and can therefore not be glued to give rise to an infinite sequence of derivatives. This would give a function which is C^n for all n, but not C^∞. We solve this issue by putting locality conditions in space and order in our definition of ContDiffWithinAt and ContDiffOn. The resulting definition is slightly more complicated to work with (in fact not so much), but it gives rise to completely satisfactory theorems.

For instance, with this definition, a real function which is C^m (but not better) on (-1/m, 1/m) for each natural m is by definition C^∞ at 0.

There is another issue with the definition of ContDiffWithinAt π•œ n f s x. We can require the existence and good behavior of derivatives up to order n on a neighborhood of x within s. However, this does not imply continuity or differentiability within s of the function at x when x does not belong to s. Therefore, we require such existence and good behavior on a neighborhood of x within s βˆͺ {x} (which appears as insert x s in this file).

Notations

We use the notation E [Γ—n]β†’L[π•œ] F for the space of continuous multilinear maps on E^n with values in F. This is the space in which the n-th derivative of a function from E to F lives.

In this file, we denote (⊀ : β„•βˆž) : WithTop β„•βˆž with ∞, and ⊀ : WithTop β„•βˆž with Ο‰. To avoid ambiguities with the two tops, the theorems name use either infty or omega. These notations are scoped in ContDiff.

Tags

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series ","### Smooth functions within a set around a point ","### Smooth functions within a set ","### Iterated derivative within a set ","### Smooth functions at a point ","### Smooth functions ","### Iterated derivative "}

ContDiffWithinAt definition
(n : WithTop β„•βˆž) (f : E β†’ F) (s : Set E) (x : E) : Prop
Full source 
/-- A function is continuously differentiable up to order `n` within a set `s` at a point `x` if
it admits continuous derivatives up to order `n` in a neighborhood of `x` in `s βˆͺ {x}`.
For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
For `n = Ο‰`, we require the function to be analytic within `s` at `x`. The precise definition we
give (all the derivatives should be analytic) is more involved to work around issues when the space
is not complete, but it is equivalent when the space is complete.

For instance, a real function which is `C^m` on `(-1/m, 1/m)` for each natural `m`, but not
better, is `C^∞` at `0` within `univ`.
-/
def ContDiffWithinAt (n : WithTop β„•βˆž) (f : E β†’ F) (s : Set E) (x : E) : Prop :=
  match n with
  | Ο‰ => βˆƒ u ∈ 𝓝[insert x s] x, βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F,
      HasFTaylorSeriesUpToOn Ο‰ f p u ∧ βˆ€ i, AnalyticOn π•œ (fun x ↦ p x i) u
  | (n : β„•βˆž) => βˆ€ m : β„•, m ≀ n β†’ βˆƒ u ∈ 𝓝[insert x s] x,
      βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpToOn m f p u
\( C^n \) differentiability within a set at a point
Informal description
A function \( f : E \to F \) is \( C^n \) within a set \( s \subseteq E \) at a point \( x \in E \) if: - For \( n = \omega \) (analytic case), there exists a neighborhood \( u \) of \( x \) in \( s \cup \{x\} \) and a formal multilinear series \( p \) such that \( f \) has a Taylor series up to order \( \omega \) on \( u \) (i.e., \( p \) represents \( f \) locally), and each coefficient \( p_i \) is analytic on \( u \). - For finite \( n \in \mathbb{N}_\infty \), for every natural number \( m \leq n \), there exists a neighborhood \( u \) of \( x \) in \( s \cup \{x\} \) and a formal multilinear series \( p \) such that \( f \) has a Taylor series up to order \( m \) on \( u \). This definition ensures that \( f \) has continuous derivatives up to order \( n \) in a neighborhood of \( x \) within \( s \cup \{x\} \), with additional analyticity conditions when \( n = \omega \).
HasFTaylorSeriesUpToOn.analyticOn theorem
(hf : HasFTaylorSeriesUpToOn Ο‰ f p s) (h : AnalyticOn π•œ (fun x ↦ p x 0) s) : AnalyticOn π•œ f s
Full source 
lemma HasFTaylorSeriesUpToOn.analyticOn
    (hf : HasFTaylorSeriesUpToOn Ο‰ f p s) (h : AnalyticOn π•œ (fun x ↦ p x 0) s) :
    AnalyticOn π•œ f s := by
  have : AnalyticOn π•œ (fun x ↦ (continuousMultilinearCurryFin0 π•œ E F) (p x 0)) s :=
    (LinearIsometryEquiv.analyticOnNhd _ _ ).comp_analyticOn
      h (Set.mapsTo_univ _ _)
  exact this.congr (fun y hy ↦ (hf.zero_eq _ hy).symm)
Analyticity from Taylor Series with Analytic Constant Term
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a formal Taylor series $p$ up to order $\omega$ (analytic) on a set $s \subseteq E$, and the constant term $x \mapsto p(x)(0)$ is analytic on $s$. Then $f$ itself is analytic on $s$.
ContDiffWithinAt.analyticOn theorem
(h : ContDiffWithinAt π•œ Ο‰ f s x) : βˆƒ u ∈ 𝓝[insert x s] x, AnalyticOn π•œ f u
Full source 
lemma ContDiffWithinAt.analyticOn (h : ContDiffWithinAt π•œ Ο‰ f s x) :
    βˆƒ u ∈ 𝓝[insert x s] x, AnalyticOn π•œ f u := by
  obtain ⟨u, hu, p, hp, h'p⟩ := h
  exact ⟨u, hu, hp.analyticOn (h'p 0)⟩
Existence of Analytic Neighborhood for \( C^\omega \) Functions Within a Set at a Point
Informal description
Let \( E \) and \( F \) be normed spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^\omega \) (analytic) within a set \( s \subseteq E \) at a point \( x \in E \), then there exists a neighborhood \( u \) of \( x \) in \( s \cup \{x\} \) such that \( f \) is analytic on \( u \).
ContDiffWithinAt.analyticWithinAt theorem
(h : ContDiffWithinAt π•œ Ο‰ f s x) : AnalyticWithinAt π•œ f s x
Full source 
lemma ContDiffWithinAt.analyticWithinAt (h : ContDiffWithinAt π•œ Ο‰ f s x) :
    AnalyticWithinAt π•œ f s x := by
  obtain ⟨u, hu, hf⟩ := h.analyticOn
  have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu
  exact (hf x xu).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)
Analyticity of \( C^\omega \) Functions Within a Set at a Point
Informal description
Let \( E \) and \( F \) be normed spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^\omega \) (analytic) within a set \( s \subseteq E \) at a point \( x \in E \), then \( f \) is analytic within \( s \) at \( x \).
contDiffWithinAt_omega_iff_analyticWithinAt theorem
[CompleteSpace F] : ContDiffWithinAt π•œ Ο‰ f s x ↔ AnalyticWithinAt π•œ f s x
Full source 
theorem contDiffWithinAt_omega_iff_analyticWithinAt [CompleteSpace F] :
    ContDiffWithinAtContDiffWithinAt π•œ Ο‰ f s x ↔ AnalyticWithinAt π•œ f s x := by
  refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩
  obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn Ο‰
  exact ⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩
Equivalence of $C^\omega$ and Analyticity for Functions on Complete Normed Spaces
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $F$ complete. For a function $f : E \to F$, a set $s \subseteq E$, and a point $x \in E$, the following are equivalent: 1. $f$ is $C^\omega$ (analytic) within $s$ at $x$; 2. $f$ is analytic within $s$ at $x$.
contDiffWithinAt_nat theorem
{n : β„•} : ContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpToOn n f p u
Full source 
theorem contDiffWithinAt_nat {n : β„•} :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x,
      βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpToOn n f p u :=
  ⟨fun H => H n le_rfl, fun ⟨u, hu, p, hp⟩ _m hm => ⟨u, hu, p, hp.of_le (mod_cast hm)⟩⟩
Characterization of $C^n$ Differentiability Within a Set at a Point via Taylor Series
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}$ a natural number. The function $f : E \to F$ is $C^n$ within $s$ at $x$ if and only if there exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ and a formal multilinear series $p : E \to \text{FormalMultilinearSeries} \mathbb{K} E F$ such that $f$ has a Taylor series up to order $n$ on $u$ represented by $p$.
contDiffWithinAt_iff_of_ne_infty theorem
(hn : n β‰  ∞) : ContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpToOn n f p u ∧ (n = Ο‰ β†’ βˆ€ i, AnalyticOn π•œ (fun x ↦ p x i) u)
Full source 
/-- When `n` is either a natural number or `Ο‰`, one can characterize the property of being `C^n`
as the existence of a neighborhood on which there is a Taylor series up to order `n`,
requiring in addition that its terms are analytic in the `Ο‰` case. -/
lemma contDiffWithinAt_iff_of_ne_infty (hn : n β‰  ∞) :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x,
      βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpToOn n f p u ∧
        (n = Ο‰ β†’ βˆ€ i, AnalyticOn π•œ (fun x ↦ p x i) u) := by
  match n with
  | Ο‰ => simp [ContDiffWithinAt]
  | ∞ => simp at hn
  | (n : β„•) => simp [contDiffWithinAt_nat]
Characterization of $C^n$ Differentiability Within a Set at a Point for $n \neq \infty$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any extended natural number $n \neq \infty$ and any point $x \in E$, the function $f$ is $C^n$ within a set $s \subseteq E$ at $x$ if and only if there exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ and a formal multilinear series $p : E \to \text{FormalMultilinearSeries} \mathbb{K} E F$ such that: 1. $p$ provides a Taylor series expansion for $f$ up to order $n$ on $u$, and 2. If $n = \omega$ (the analytic case), then for each $i$, the coefficient function $x \mapsto p(x)_i$ is analytic on $u$.
ContDiffWithinAt.of_le theorem
(h : ContDiffWithinAt π•œ n f s x) (hmn : m ≀ n) : ContDiffWithinAt π•œ m f s x
Full source 
theorem ContDiffWithinAt.of_le (h : ContDiffWithinAt π•œ n f s x) (hmn : m ≀ n) :
    ContDiffWithinAt π•œ m f s x := by
  match n with
  | Ο‰ => match m with
    | Ο‰ => exact h
    | (m : β„•βˆž) =>
      intro k _
      obtain ⟨u, hu, p, hp, -⟩ := h
      exact ⟨u, hu, p, hp.of_le le_top⟩
  | (n : β„•βˆž) => match m with
    | Ο‰ => simp at hmn
    | (m : β„•βˆž) => exact fun k hk ↦ h k (le_trans hk (mod_cast hmn))
Decreasing Differentiability Order for $C^n$ Functions Within a Set at a Point
Informal description
Let $f : E \to F$ be a function between normed vector spaces over a nontrivially normed field $\mathbb{K}$. If $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$, and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then $f$ is $C^m$ within $s$ at $x$.
AnalyticWithinAt.contDiffWithinAt theorem
[CompleteSpace F] (h : AnalyticWithinAt π•œ f s x) : ContDiffWithinAt π•œ n f s x
Full source 
/-- In a complete space, a function which is analytic within a set at a point is also `C^Ο‰` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`. -/
theorem AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] (h : AnalyticWithinAt π•œ f s x) :
    ContDiffWithinAt π•œ n f s x :=
  (contDiffWithinAt_omega_iff_analyticWithinAt.2 h).of_le le_top
Analyticity implies \( C^n \) differentiability in complete spaces
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), with \( F \) complete. If a function \( f : E \to F \) is analytic within a set \( s \subseteq E \) at a point \( x \in E \), then \( f \) is \( C^n \) within \( s \) at \( x \) for any extended natural number \( n \).
contDiffWithinAt_iff_forall_nat_le theorem
{n : β„•βˆž} : ContDiffWithinAt π•œ n f s x ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiffWithinAt π•œ m f s x
Full source 
theorem contDiffWithinAt_iff_forall_nat_le {n : β„•βˆž} :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiffWithinAt π•œ m f s x :=
  ⟨fun H _ hm => H.of_le (mod_cast hm), fun H m hm => H m hm _ le_rfl⟩
Characterization of $C^n$ Differentiability Within a Set at a Point via Finite Differentiability Orders
Informal description
Let $f : E \to F$ be a function between normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}_\infty$ an extended natural number. Then $f$ is $C^n$ within $s$ at $x$ if and only if for every natural number $m$ with $m \leq n$, $f$ is $C^m$ within $s$ at $x$.
contDiffWithinAt_infty theorem
: ContDiffWithinAt π•œ ∞ f s x ↔ βˆ€ n : β„•, ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_infty :
    ContDiffWithinAtContDiffWithinAt π•œ ∞ f s x ↔ βˆ€ n : β„•, ContDiffWithinAt π•œ n f s x :=
  contDiffWithinAt_iff_forall_nat_le.trans <| by simp only [forall_prop_of_true, le_top]
Characterization of \( C^\infty \) Differentiability Within a Set at a Point via Finite Differentiability Orders
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^\infty \) within a set \( s \subseteq E \) at a point \( x \in E \) if and only if it is \( C^n \) within \( s \) at \( x \) for every natural number \( n \).
ContDiffWithinAt.continuousWithinAt theorem
(h : ContDiffWithinAt π•œ n f s x) : ContinuousWithinAt f s x
Full source 
theorem ContDiffWithinAt.continuousWithinAt (h : ContDiffWithinAt π•œ n f s x) :
    ContinuousWithinAt f s x := by
  have := h.of_le (zero_le _)
  simp only [ContDiffWithinAt, nonpos_iff_eq_zero, Nat.cast_eq_zero,
    mem_pure, forall_eq, CharP.cast_eq_zero] at this
  rcases this with ⟨u, hu, p, H⟩
  rw [mem_nhdsWithin_insert] at hu
  exact (H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2
$C^n$ differentiability implies continuity within a set at a point
Informal description
Let $f : E \to F$ be a function between normed vector spaces over a nontrivially normed field $\mathbb{K}$. If $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$, then $f$ is continuous within $s$ at $x$.
ContDiffWithinAt.congr_of_eventuallyEq theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr_of_eventuallyEq (h : ContDiffWithinAt π•œ n f s x)
    (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x := by
  match n with
  | Ο‰ =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, hβ‚βŸ©), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩
  | (n : β„•βˆž) =>
    intro m hm
    let ⟨u, hu, p, H⟩ := h m hm
    exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, hβ‚βŸ©), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩
Preservation of \( C^n \) Differentiability under Eventual Equality within a Set at a Point
Informal description
Let \( f, f_1 : E \to F \) be functions between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( s \subseteq E \) be a subset. Suppose that \( f \) is \( C^n \) within \( s \) at a point \( x \in E \). If \( f_1 \) is eventually equal to \( f \) in a neighborhood of \( x \) within \( s \), and \( f_1(x) = f(x) \), then \( f_1 \) is also \( C^n \) within \( s \) at \( x \).
Filter.EventuallyEq.congr_contDiffWithinAt theorem
(h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem Filter.EventuallyEq.congr_contDiffWithinAt (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) :
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  ⟨fun H ↦ H.congr_of_eventuallyEq h₁.symm hx.symm, fun H ↦ H.congr_of_eventuallyEq h₁ hx⟩
Equivalence of \( C^n \) Differentiability under Eventual Equality within a Set at a Point
Informal description
Let \( f, f_1 : E \to F \) be functions between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( s \subseteq E \) be a subset. Suppose that \( f_1 \) is eventually equal to \( f \) in a neighborhood of \( x \) within \( s \), and \( f_1(x) = f(x) \). Then \( f_1 \) is \( C^n \) within \( s \) at \( x \) if and only if \( f \) is \( C^n \) within \( s \) at \( x \).
ContDiffWithinAt.congr_of_eventuallyEq_insert theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [𝓝[insert x s] x] f) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr_of_eventuallyEq_insert (h : ContDiffWithinAt π•œ n f s x)
    (h₁ : f₁ =αΆ [𝓝[insert x s] x] f) : ContDiffWithinAt π•œ n f₁ s x :=
  h.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) h₁)
    (mem_of_mem_nhdsWithin (mem_insert x s) h₁ :)
Preservation of $C^n$ Differentiability under Eventual Equality in Extended Neighborhood
Informal description
Let $f, f_1 : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose that $f$ is $C^n$ within $s$ at a point $x \in E$. If $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s \cup \{x\}$, then $f_1$ is also $C^n$ within $s$ at $x$.
Filter.EventuallyEq.congr_contDiffWithinAt_of_insert theorem
(h₁ : f₁ =αΆ [𝓝[insert x s] x] f) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem Filter.EventuallyEq.congr_contDiffWithinAt_of_insert (h₁ : f₁ =αΆ [𝓝[insert x s] x] f) :
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  ⟨fun H ↦ H.congr_of_eventuallyEq_insert h₁.symm, fun H ↦ H.congr_of_eventuallyEq_insert hβ‚βŸ©
Equivalence of $C^n$ Differentiability under Eventual Equality in Extended Neighborhood
Informal description
Let $f, f_1 : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s \cup \{x\}$, then $f_1$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
ContDiffWithinAt.congr_of_eventuallyEq_of_mem theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr_of_eventuallyEq_of_mem (h : ContDiffWithinAt π•œ n f s x)
    (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x :=
  h.congr_of_eventuallyEq h₁ <| h₁.self_of_nhdsWithin hx
Preservation of $C^n$ Differentiability under Eventual Equality at a Point in a Set
Informal description
Let $f, f_1 : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose that $f$ is $C^n$ within $s$ at a point $x \in s$. If $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s$, then $f_1$ is also $C^n$ within $s$ at $x$.
Filter.EventuallyEq.congr_contDiffWithinAt_of_mem theorem
(h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem Filter.EventuallyEq.congr_contDiffWithinAt_of_mem (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s):
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  ⟨fun H ↦ H.congr_of_eventuallyEq_of_mem h₁.symm hx, fun H ↦ H.congr_of_eventuallyEq_of_mem h₁ hx⟩
Equivalence of $C^n$ Differentiability under Eventual Equality within a Set at a Point
Informal description
Let $f, f_1 : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For a point $x \in s$, if $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s$, then $f_1$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
ContDiffWithinAt.congr theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr (h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y)
    (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x :=
  h.congr_of_eventuallyEq (Filter.eventuallyEq_of_mem self_mem_nhdsWithin h₁) hx
Preservation of $C^n$ Differentiability under Pointwise Equality within a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$. Suppose $f : E \to F$ is $C^n$ within $s$ at $x$. If $f_1 : E \to F$ satisfies $f_1(y) = f(y)$ for all $y \in s$ and $f_1(x) = f(x)$, then $f_1$ is also $C^n$ within $s$ at $x$.
contDiffWithinAt_congr theorem
(h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_congr (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  ⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦  h'.congr h₁ hx⟩
Equivalence of $C^n$ Differentiability Under Pointwise Equality Within a Set at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$. For two functions $f, f_1 : E \to F$, if $f_1(y) = f(y)$ for all $y \in s$ and $f_1(x) = f(x)$, then $f_1$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
ContDiffWithinAt.congr_of_mem theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr_of_mem (h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y)
    (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x :=
  h.congr h₁ (h₁ _ hx)
Preservation of $C^n$ Differentiability under Pointwise Equality within a Set for Points in the Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in s$. Suppose $f : E \to F$ is $C^n$ within $s$ at $x$. If $f_1 : E \to F$ satisfies $f_1(y) = f(y)$ for all $y \in s$, then $f_1$ is also $C^n$ within $s$ at $x$.
contDiffWithinAt_congr_of_mem theorem
(h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : x ∈ s) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_congr_of_mem (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  contDiffWithinAt_congr h₁ (h₁ x hx)
Equivalence of $C^n$ Differentiability Under Pointwise Equality Within a Set for Points in the Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in s$. For two functions $f, f_1 : E \to F$, if $f_1(y) = f(y)$ for all $y \in s$, then $f_1$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
ContDiffWithinAt.congr_of_insert theorem
(h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ insert x s, f₁ y = f y) : ContDiffWithinAt π•œ n f₁ s x
Full source 
theorem ContDiffWithinAt.congr_of_insert (h : ContDiffWithinAt π•œ n f s x)
    (h₁ : βˆ€ y ∈ insert x s, f₁ y = f y) : ContDiffWithinAt π•œ n f₁ s x :=
  h.congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))
Preservation of $C^n$ Differentiability Under Pointwise Equality on $s \cup \{x\}$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$. If $f : E \to F$ is $C^n$ within $s$ at $x$, and $f_1 : E \to F$ satisfies $f_1(y) = f(y)$ for all $y \in s \cup \{x\}$, then $f_1$ is also $C^n$ within $s$ at $x$.
contDiffWithinAt_congr_of_insert theorem
(h₁ : βˆ€ y ∈ insert x s, f₁ y = f y) : ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_congr_of_insert (h₁ : βˆ€ y ∈ insert x s, f₁ y = f y) :
    ContDiffWithinAtContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x :=
  contDiffWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))
Equivalence of $C^n$ Differentiability Under Pointwise Equality on $s \cup \{x\}$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$. For two functions $f, f_1 : E \to F$, if $f_1(y) = f(y)$ for all $y \in s \cup \{x\}$, then $f_1$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
ContDiffWithinAt.mono_of_mem_nhdsWithin theorem
(h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : s ∈ 𝓝[t] x) : ContDiffWithinAt π•œ n f t x
Full source 
theorem ContDiffWithinAt.mono_of_mem_nhdsWithin (h : ContDiffWithinAt π•œ n f s x) {t : Set E}
    (hst : s ∈ 𝓝[t] x) : ContDiffWithinAt π•œ n f t x := by
  match n with
  | Ο‰ =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩
  | (n : β„•βˆž) =>
    intro m hm
    rcases h m hm with ⟨u, hu, p, H⟩
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩
Local \( C^n \) Differentiability is Preserved Under Neighborhood Refinement
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. Suppose \( f \) is \( C^n \) within a set \( s \subseteq E \) at a point \( x \in E \). If \( s \) is a neighborhood of \( x \) within another set \( t \subseteq E \) (i.e., \( s \in \mathcal{N}_t(x) \)), then \( f \) is \( C^n \) within \( t \) at \( x \).
ContDiffWithinAt.mono theorem
(h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : t βŠ† s) : ContDiffWithinAt π•œ n f t x
Full source 
theorem ContDiffWithinAt.mono (h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : t βŠ† s) :
    ContDiffWithinAt π•œ n f t x :=
  h.mono_of_mem_nhdsWithin <| Filter.mem_of_superset self_mem_nhdsWithin hst
$C^n$ Differentiability is Preserved Under Subset Restriction
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$, then for any subset $t \subseteq s$, the function $f$ is also $C^n$ within $t$ at $x$.
ContDiffWithinAt.congr_mono theorem
(h : ContDiffWithinAt π•œ n f s x) (h' : EqOn f₁ f s₁) (h₁ : s₁ βŠ† s) (hx : f₁ x = f x) : ContDiffWithinAt π•œ n f₁ s₁ x
Full source 
theorem ContDiffWithinAt.congr_mono
    (h : ContDiffWithinAt π•œ n f s x) (h' : EqOn f₁ f s₁) (h₁ : s₁ βŠ† s) (hx : f₁ x = f x) :
    ContDiffWithinAt π•œ n f₁ s₁ x :=
  (h.mono h₁).congr h' hx
Preservation of \( C^n \) Differentiability under Pointwise Equality and Subset Restriction
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function that is \( C^n \) within a set \( s \subseteq E \) at a point \( x \in E \). If \( f_1 : E \to F \) coincides with \( f \) on a subset \( s_1 \subseteq s \) (i.e., \( f_1(y) = f(y) \) for all \( y \in s_1 \)) and \( f_1(x) = f(x) \), then \( f_1 \) is also \( C^n \) within \( s_1 \) at \( x \).
ContDiffWithinAt.congr_set theorem
(h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : s =αΆ [𝓝 x] t) : ContDiffWithinAt π•œ n f t x
Full source 
theorem ContDiffWithinAt.congr_set (h : ContDiffWithinAt π•œ n f s x) {t : Set E}
    (hst : s =αΆ [𝓝 x] t) : ContDiffWithinAt π•œ n f t x := by
  rw [← nhdsWithin_eq_iff_eventuallyEq] at hst
  apply h.mono_of_mem_nhdsWithin <| hst β–Έ self_mem_nhdsWithin
$C^n$ Differentiability Within Sets is Preserved Under Eventual Set Equality
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$. If $s$ and $t$ are eventually equal in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$), then $f$ is $C^n$ within $t$ at $x$.
contDiffWithinAt_congr_set theorem
{t : Set E} (hst : s =αΆ [𝓝 x] t) : ContDiffWithinAt π•œ n f s x ↔ ContDiffWithinAt π•œ n f t x
Full source 
theorem contDiffWithinAt_congr_set {t : Set E} (hst : s =αΆ [𝓝 x] t) :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ ContDiffWithinAt π•œ n f t x :=
  ⟨fun h => h.congr_set hst, fun h => h.congr_set hst.symm⟩
$C^n$ Differentiability Within Sets is Equivalent Under Eventual Set Equality
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any sets $s, t \subseteq E$ and a point $x \in E$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ (i.e., $s =_{\mathcal{N}(x)} t$), then $f$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ within $t$ at $x$.
contDiffWithinAt_inter' theorem
(h : t ∈ 𝓝[s] x) : ContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    ContDiffWithinAtContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x :=
  contDiffWithinAt_congr_set (mem_nhdsWithin_iff_eventuallyEq.1 h).symm
$C^n$ Differentiability Within Intersection of Sets is Equivalent to Original Set When One is a Neighborhood
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any sets $s, t \subseteq E$ and a point $x \in E$, if $t$ belongs to the neighborhood filter of $x$ within $s$ (i.e., $t \in \mathcal{N}_s(x)$), then $f$ is $C^n$ within $s \cap t$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
contDiffWithinAt_inter theorem
(h : t ∈ 𝓝 x) : ContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_inter (h : t ∈ 𝓝 x) :
    ContDiffWithinAtContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x :=
  contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds h)
$C^n$ Differentiability Within Intersection of Sets is Equivalent to Original Set When One is a Neighborhood
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any sets $s, t \subseteq E$ and a point $x \in E$, if $t$ is a neighborhood of $x$, then $f$ is $C^n$ within $s \cap t$ at $x$ if and only if $f$ is $C^n$ within $s$ at $x$.
contDiffWithinAt_insert_self theorem
: ContDiffWithinAt π•œ n f (insert x s) x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_insert_self :
    ContDiffWithinAtContDiffWithinAt π•œ n f (insert x s) x ↔ ContDiffWithinAt π•œ n f s x := by
  match n with
  | Ο‰ => simp [ContDiffWithinAt]
  | (n : β„•βˆž) => simp_rw [ContDiffWithinAt, insert_idem]
Equivalence of \( C^n \) Differentiability at a Point with and without Insertion of the Point into the Set
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and for any extended natural number \( n \), the function \( f \) is \( C^n \) within the set \( \{x\} \cup s \) at the point \( x \) if and only if it is \( C^n \) within the set \( s \) at \( x \).
contDiffWithinAt_insert theorem
{y : E} : ContDiffWithinAt π•œ n f (insert y s) x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_insert {y : E} :
    ContDiffWithinAtContDiffWithinAt π•œ n f (insert y s) x ↔ ContDiffWithinAt π•œ n f s x := by
  rcases eq_or_ne x y with (rfl | hx)
  Β· exact contDiffWithinAt_insert_self
  refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
  apply h.mono_of_mem_nhdsWithin
  simp [nhdsWithin_insert_of_ne hx, self_mem_nhdsWithin]
\( C^n \) Differentiability at a Point is Unaffected by Insertion of a Point into the Set
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), a point \( x \in E \), a set \( s \subseteq E \), and an extended natural number \( n \), the function \( f \) is \( C^n \) within the set \( \{y\} \cup s \) at \( x \) if and only if it is \( C^n \) within \( s \) at \( x \).
ContDiffWithinAt.insert theorem
(h : ContDiffWithinAt π•œ n f s x) : ContDiffWithinAt π•œ n f (insert x s) x
Full source 
protected theorem ContDiffWithinAt.insert (h : ContDiffWithinAt π•œ n f s x) :
    ContDiffWithinAt π•œ n f (insert x s) x :=
  h.insert'
Preservation of \( C^n \) Differentiability under Set Insertion at a Point
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), \( s \subseteq E \) a subset, and \( x \in E \) a point. If a function \( f : E \to F \) is \( C^n \) within \( s \) at \( x \), then \( f \) is also \( C^n \) within \( s \cup \{x\} \) at \( x \).
contDiffWithinAt_diff_singleton theorem
{y : E} : ContDiffWithinAt π•œ n f (s \ { y }) x ↔ ContDiffWithinAt π•œ n f s x
Full source 
theorem contDiffWithinAt_diff_singleton {y : E} :
    ContDiffWithinAtContDiffWithinAt π•œ n f (s \ {y}) x ↔ ContDiffWithinAt π•œ n f s x := by
  rw [← contDiffWithinAt_insert, insert_diff_singleton, contDiffWithinAt_insert]
\( C^n \) Differentiability at a Point is Unaffected by Removal of a Point from the Set
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), a point \( x \in E \), a set \( s \subseteq E \), and an extended natural number \( n \), the function \( f \) is \( C^n \) within the set \( s \setminus \{y\} \) at \( x \) if and only if it is \( C^n \) within \( s \) at \( x \).
ContDiffWithinAt.differentiableWithinAt' theorem
(h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) : DifferentiableWithinAt π•œ f (insert x s) x
Full source 
/-- If a function is `C^n` within a set at a point, with `n β‰₯ 1`, then it is differentiable
within this set at this point. -/
theorem ContDiffWithinAt.differentiableWithinAt' (h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) :
    DifferentiableWithinAt π•œ f (insert x s) x := by
  rcases contDiffWithinAt_nat.1 (h.of_le hn) with ⟨u, hu, p, H⟩
  rcases mem_nhdsWithin.1 hu with ⟨t, t_open, xt, tu⟩
  rw [inter_comm] at tu
  exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 <|
    ((H.mono tu).differentiableOn le_rfl) x ⟨mem_insert x s, xt⟩
Differentiability of $C^n$ functions within an augmented set at a point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}_\infty$ with $1 \leq n$. If a function $f : E \to F$ is $C^n$ within $s$ at $x$, then $f$ is differentiable within $s \cup \{x\}$ at $x$.
ContDiffWithinAt.differentiableWithinAt theorem
(h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) : DifferentiableWithinAt π•œ f s x
Full source 
theorem ContDiffWithinAt.differentiableWithinAt (h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) :
    DifferentiableWithinAt π•œ f s x :=
  (h.differentiableWithinAt' hn).mono (subset_insert x s)
Differentiability of $C^n$ functions within a set at a point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}_\infty$ with $1 \leq n$. If a function $f : E \to F$ is $C^n$ within $s$ at $x$, then $f$ is differentiable within $s$ at $x$.
contDiffWithinAt_succ_iff_hasFDerivWithinAt theorem
(hn : n β‰  ∞) : ContDiffWithinAt π•œ (n + 1) f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧ βˆƒ f' : E β†’ E β†’L[π•œ] F, (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt π•œ n f' u x
Full source 
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`
(and moreover the function is analytic when `n = Ο‰`). -/
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt (hn : n β‰  ∞) :
    ContDiffWithinAtContDiffWithinAt π•œ (n + 1) f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧
      βˆƒ f' : E β†’ E β†’L[π•œ] F,
      (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt π•œ n f' u x := by
  have h'n : n + 1 β‰  ∞ := by simpa using hn
  constructor
  Β· intro h
    rcases (contDiffWithinAt_iff_of_ne_infty h'n).1 h with ⟨u, hu, p, Hp, H'p⟩
    refine ⟨u, hu, ?_, fun y => (continuousMultilinearCurryFin1 π•œ E F) (p y 1),
        fun y hy => Hp.hasFDerivWithinAt le_add_self hy, ?_⟩
    Β· rintro rfl
      exact Hp.analyticOn (H'p rfl 0)
    apply (contDiffWithinAt_iff_of_ne_infty hn).2
    refine ⟨u, ?_, fun y : E => (p y).shift, ?_⟩
    Β· convert @self_mem_nhdsWithin _ _ x u
      have : x ∈ insert x s := by simp
      exact insert_eq_of_mem (mem_of_mem_nhdsWithin this hu)
    Β· rw [hasFTaylorSeriesUpToOn_succ_iff_right] at Hp
      refine ⟨Hp.2.2, ?_⟩
      rintro rfl i
      change AnalyticOn π•œ
        (fun x ↦ (continuousMultilinearCurryRightEquiv' π•œ i E F) (p x (i + 1))) u
      apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
        ?_ (Set.mapsTo_univ _ _)
      exact H'p rfl _
  · rintro ⟨u, hu, hf, f', f'_eq_deriv, Hf'⟩
    rw [contDiffWithinAt_iff_of_ne_infty h'n]
    rcases (contDiffWithinAt_iff_of_ne_infty hn).1 Hf' with ⟨v, hv, p', Hp', p'_an⟩
    refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩
    Β· apply Filter.inter_mem _ hu
      apply nhdsWithin_le_of_mem hu
      exact nhdsWithin_mono _ (subset_insert x u) hv
    Β· rw [hasFTaylorSeriesUpToOn_succ_iff_right]
      refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩
      Β· change
          HasFDerivWithinAt (fun z => (continuousMultilinearCurryFin0 π•œ E F).symm (f z))
            (FormalMultilinearSeries.unshift (p' y) (f y) 1).curryLeft (v ∩ u) y
        rw [← Function.comp_def _ f, LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
        convert (f'_eq_deriv y hy.2).mono inter_subset_right
        rw [← Hp'.zero_eq y hy.1]
        ext z
        change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) =
          ((p' y 0) 0) z
        congr
        norm_num [eq_iff_true_of_subsingleton]
      Β· convert (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1
        Β· ext x y
          change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y
          rw [init_snoc]
        Β· ext x k v y
          change p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y))
            (@snoc k (fun _ : Fin k.succ => E) v y (last k)) = p' x k v y
          rw [snoc_last, init_snoc]
    Β· intro h i
      simp only [WithTop.add_eq_top, WithTop.one_ne_top, or_false] at h
      match i with
      | 0 =>
        simp only [FormalMultilinearSeries.unshift]
        apply AnalyticOnNhd.comp_analyticOn _ ((hf h).mono inter_subset_right)
          (Set.mapsTo_univ _ _)
        exact LinearIsometryEquiv.analyticOnNhd _ _
      | i + 1 =>
        simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one]
        apply AnalyticOnNhd.comp_analyticOn _ ((p'_an h i).mono inter_subset_left)
          (Set.mapsTo_univ _ _)
        exact LinearIsometryEquiv.analyticOnNhd _ _
Characterization of $C^{n+1}$ Differentiability via Local Existence of $C^n$ Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}_\infty$ with $n \neq \infty$. Then the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ within $s$ at $x$. 2. There exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ such that: - If $n = \omega$, then $f$ is analytic on $u$. - There exists a derivative function $f' : E \to (E \toL[\mathbb{K}] F)$ such that: * For all $y \in u$, $f$ has FrΓ©chet derivative $f'(y)$ within $u$ at $y$. * $f'$ is $C^n$ within $u$ at $x$.
contDiffWithinAt_succ_iff_hasFDerivWithinAt' theorem
(hn : n β‰  ∞) : ContDiffWithinAt π•œ (n + 1) f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, u βŠ† insert x s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧ βˆƒ f' : E β†’ E β†’L[π•œ] F, (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt π•œ n f' s x
Full source 
/-- A version of `contDiffWithinAt_succ_iff_hasFDerivWithinAt` where all derivatives
  are taken within the same set. -/
theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt' (hn : n β‰  ∞) :
    ContDiffWithinAtContDiffWithinAt π•œ (n + 1) f s x ↔
      βˆƒ u ∈ 𝓝[insert x s] x, u βŠ† insert x s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧
      βˆƒ f' : E β†’ E β†’L[π•œ] F,
        (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt π•œ n f' s x := by
  refine ⟨fun hf => ?_, ?_⟩
  · obtain ⟨u, hu, f_an, f', huf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).mp hf
    obtain ⟨w, hw, hxw, hwu⟩ := mem_nhdsWithin.mp hu
    rw [inter_comm] at hwu
    refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f',
      fun y hy => ?_, ?_⟩
    Β· intro h
      apply (f_an h).mono hwu
    Β· refine ((huf' y <| hwu hy).mono hwu).mono_of_mem_nhdsWithin ?_
      refine mem_of_superset ?_ (inter_subset_inter_left _ (subset_insert _ _))
      exact inter_mem_nhdsWithin _ (hw.mem_nhds hy.2)
    Β· exact hf'.mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)
  Β· rw [← contDiffWithinAt_insert, contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem (mem_insert _ _)]
    rintro ⟨u, hu, hus, f_an, f', huf', hf'⟩
    exact ⟨u, hu, f_an, f', fun y hy => (huf' y hy).insert'.mono hus, hf'.insert.mono hus⟩
Characterization of $C^{n+1}$ Differentiability via Local Existence of $C^n$ Derivative (Restricted Set Version)
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, $x \in E$ a point, and $n \in \mathbb{N}_\infty$ with $n \neq \infty$. Then the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ within $s$ at $x$. 2. There exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ such that: - $u \subseteq s \cup \{x\}$, - If $n = \omega$, then $f$ is analytic on $u$, - There exists a derivative function $f' : E \to (E \toL[\mathbb{K}] F)$ such that: * For all $y \in u$, $f$ has FrΓ©chet derivative $f'(y)$ within $s$ at $y$, * $f'$ is $C^n$ within $s$ at $x$.
ContDiffOn definition
(n : WithTop β„•βˆž) (f : E β†’ F) (s : Set E) : Prop
Full source 
/-- A function is continuously differentiable up to `n` on `s` if, for any point `x` in `s`, it
admits continuous derivatives up to order `n` on a neighborhood of `x` in `s`.

For `n = ∞`, we only require that this holds up to any finite order (where the neighborhood may
depend on the finite order we consider).
-/
def ContDiffOn (n : WithTop β„•βˆž) (f : E β†’ F) (s : Set E) : Prop :=
  βˆ€ x ∈ s, ContDiffWithinAt π•œ n f s x
\( C^n \) differentiability on a set
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is said to be \( C^n \) on a set \( s \subseteq E \) (denoted by `ContDiffOn π•œ n f s`) if for every point \( x \in s \), the function \( f \) is \( C^n \) within \( s \) at \( x \). For finite \( n \), this means that \( f \) has continuous derivatives up to order \( n \) in a neighborhood of \( x \) within \( s \cup \{x\} \). For \( n = \infty \), this holds for all finite \( n \), and for \( n = \omega \) (the analytic case), \( f \) is analytic on \( s \).
HasFTaylorSeriesUpToOn.contDiffOn theorem
{n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F} (hf : HasFTaylorSeriesUpToOn n f f' s) : ContDiffOn π•œ n f s
Full source 
theorem HasFTaylorSeriesUpToOn.contDiffOn {n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F}
    (hf : HasFTaylorSeriesUpToOn n f f' s) : ContDiffOn π•œ n f s := by
  intro x hx m hm
  use s
  simp only [Set.insert_eq_of_mem hx, self_mem_nhdsWithin, true_and]
  exact ⟨f', hf.of_le (mod_cast hm)⟩
Existence of Taylor Series Implies $C^n$ Differentiability on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a formal Taylor series expansion $f'$ up to order $n$ on a set $s \subseteq E$ (i.e., `HasFTaylorSeriesUpToOn n f f' s` holds), then $f$ is $C^n$ on $s$ (i.e., `ContDiffOn π•œ n f s` holds).
ContDiffOn.contDiffWithinAt theorem
(h : ContDiffOn π•œ n f s) (hx : x ∈ s) : ContDiffWithinAt π•œ n f s x
Full source 
theorem ContDiffOn.contDiffWithinAt (h : ContDiffOn π•œ n f s) (hx : x ∈ s) :
    ContDiffWithinAt π•œ n f s x :=
  h x hx
Local \( C^n \) Differentiability from Global \( C^n \) Differentiability on a Set
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^n \) on a set \( s \subseteq E \) (i.e., \( \text{ContDiffOn} \, \mathbb{K} \, n \, f \, s \) holds), then for any point \( x \in s \), the function \( f \) is \( C^n \) within \( s \) at \( x \) (i.e., \( \text{ContDiffWithinAt} \, \mathbb{K} \, n \, f \, s \, x \) holds).
ContDiffOn.of_le theorem
(h : ContDiffOn π•œ n f s) (hmn : m ≀ n) : ContDiffOn π•œ m f s
Full source 
theorem ContDiffOn.of_le (h : ContDiffOn π•œ n f s) (hmn : m ≀ n) : ContDiffOn π•œ m f s := fun x hx =>
  (h x hx).of_le hmn
Decreasing Differentiability Order for $C^n$ Functions on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ on a set $s \subseteq E$ (i.e., $f$ is $n$-times continuously differentiable on $s$), and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then $f$ is $C^m$ on $s$.
ContDiffWithinAt.contDiffOn' theorem
(hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰) (h : ContDiffWithinAt π•œ n f s x) : βˆƒ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ m f (insert x s ∩ u)
Full source 
theorem ContDiffWithinAt.contDiffOn' (hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰)
    (h : ContDiffWithinAt π•œ n f s x) :
    βˆƒ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ m f (insert x s ∩ u) := by
  rcases eq_or_ne n Ο‰ with rfl | hn
  · obtain ⟨t, ht, p, hp, h'p⟩ := h
    rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
    rw [inter_comm] at hut
    refine ⟨u, huo, hxu, ?_⟩
    suffices ContDiffOn π•œ Ο‰ f (insertinsert x s ∩ u) from this.of_le le_top
    intro y hy
    refine ⟨insert x s ∩ u, ?_, p, hp.mono hut,  fun i ↦ (h'p i).mono hut⟩
    simp only [insert_eq_of_mem, hy, self_mem_nhdsWithin]
  Β· match m with
    | Ο‰ => simp [hn] at hm
    | ∞ => exact (hn (h' rfl)).elim
    | (m : β„•) =>
      rcases contDiffWithinAt_nat.1 (h.of_le hm) with ⟨t, ht, p, hp⟩
      rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
      rw [inter_comm] at hut
      exact ⟨u, huo, hxu, (hp.mono hut).contDiffOn⟩
Local $C^m$ Differentiability from $C^n$ Differentiability at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$ a point. If $f : E \to F$ is $C^n$ within $s$ at $x$, and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$ (with the condition that if $m = \infty$ then $n = \omega$), then there exists an open neighborhood $u$ of $x$ such that $f$ is $C^m$ on the intersection of $u$ with $s \cup \{x\}$.
ContDiffWithinAt.contDiffOn theorem
(hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰) (h : ContDiffWithinAt π•œ n f s x) : βˆƒ u ∈ 𝓝[insert x s] x, u βŠ† insert x s ∧ ContDiffOn π•œ m f u
Full source 
theorem ContDiffWithinAt.contDiffOn (hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰)
    (h : ContDiffWithinAt π•œ n f s x) :
    βˆƒ u ∈ 𝓝[insert x s] x, u βŠ† insert x s ∧ ContDiffOn π•œ m f u := by
  obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'
  exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩
Local $C^m$ Differentiability from $C^n$ Differentiability at a Point (Neighborhood Version)
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$ a point. If $f : E \to F$ is $C^n$ within $s$ at $x$, and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$ (with the condition that if $m = \infty$ then $n = \omega$), then there exists a neighborhood $u$ of $x$ within $s \cup \{x\}$ such that $f$ is $C^m$ on $u$ and $u \subseteq s \cup \{x\}$.
ContDiffOn.analyticOn theorem
(h : ContDiffOn π•œ Ο‰ f s) : AnalyticOn π•œ f s
Full source 
theorem ContDiffOn.analyticOn (h : ContDiffOn π•œ Ο‰ f s) : AnalyticOn π•œ f s :=
  fun x hx ↦ (h x hx).analyticWithinAt
Analyticity of \( C^\omega \) Functions on a Set
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^\omega \) (i.e., analytic) on a set \( s \subseteq E \), then \( f \) is analytic on \( s \).
contDiffWithinAt_iff_contDiffOn_nhds theorem
(hn : n β‰  ∞) : ContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, ContDiffOn π•œ n f u
Full source 
/-- A function is `C^n` within a set at a point, for `n : β„•`, if and only if it is `C^n` on
a neighborhood of this point. -/
theorem contDiffWithinAt_iff_contDiffOn_nhds (hn : n β‰  ∞) :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ βˆƒ u ∈ 𝓝[insert x s] x, ContDiffOn π•œ n f u := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, h'u⟩
    exact ⟨u, hu, h'u.2⟩
  · rcases h with ⟨u, u_mem, hu⟩
    have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert x s) u_mem
    exact (hu x this).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert x s) u_mem)
Characterization of $C^n$ Differentiability Within a Set at a Point via Neighborhoods
Informal description
For a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, a set $s \subseteq E$, a point $x \in E$, and an extended natural number $n \neq \infty$, the following are equivalent: 1. $f$ is $C^n$ within $s$ at $x$. 2. There exists a neighborhood $u$ of $x$ within $s \cup \{x\}$ such that $f$ is $C^n$ on $u$. Here, $f$ being $C^n$ within $s$ at $x$ means that $f$ has continuous derivatives up to order $n$ in a neighborhood of $x$ within $s \cup \{x\}$.
ContDiffWithinAt.eventually theorem
(h : ContDiffWithinAt π•œ n f s x) (hn : n β‰  ∞) : βˆ€αΆ  y in 𝓝[insert x s] x, ContDiffWithinAt π•œ n f s y
Full source 
protected theorem ContDiffWithinAt.eventually (h : ContDiffWithinAt π•œ n f s x) (hn : n β‰  ∞) :
    βˆ€αΆ  y in 𝓝[insert x s] x, ContDiffWithinAt π•œ n f s y := by
  rcases h.contDiffOn le_rfl (by simp [hn]) with ⟨u, hu, _, hd⟩
  have : βˆ€αΆ  y : E in 𝓝[insert x s] x, u ∈ 𝓝[insert x s] y ∧ y ∈ u :=
    (eventually_eventually_nhdsWithin.2 hu).and hu
  refine this.mono fun y hy => (hd y hy.2).mono_of_mem_nhdsWithin ?_
  exact nhdsWithin_mono y (subset_insert _ _) hy.1
Local persistence of $C^n$ differentiability within a set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$ (where $n \neq \infty$), then for all points $y$ in a sufficiently small neighborhood of $x$ within $s \cup \{x\}$, the function $f$ is also $C^n$ within $s$ at $y$.
ContDiffOn.of_succ theorem
(h : ContDiffOn π•œ (n + 1) f s) : ContDiffOn π•œ n f s
Full source 
theorem ContDiffOn.of_succ (h : ContDiffOn π•œ (n + 1) f s) : ContDiffOn π•œ n f s :=
  h.of_le le_self_add
Decreasing Differentiability Order for $C^{n+1}$ Functions on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^{n+1}$ on a set $s \subseteq E$ (i.e., $f$ is $(n+1)$-times continuously differentiable on $s$), then $f$ is $C^n$ on $s$.
ContDiffOn.one_of_succ theorem
(h : ContDiffOn π•œ (n + 1) f s) : ContDiffOn π•œ 1 f s
Full source 
theorem ContDiffOn.one_of_succ (h : ContDiffOn π•œ (n + 1) f s) : ContDiffOn π•œ 1 f s :=
  h.of_le le_add_self
$C^{n+1}$ implies $C^1$ on a set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^{n+1}$ on a set $s \subseteq E$ (i.e., $f$ is $(n+1)$-times continuously differentiable on $s$), then $f$ is $C^1$ on $s$.
contDiffOn_iff_forall_nat_le theorem
{n : β„•βˆž} : ContDiffOn π•œ n f s ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiffOn π•œ m f s
Full source 
theorem contDiffOn_iff_forall_nat_le {n : β„•βˆž} :
    ContDiffOnContDiffOn π•œ n f s ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiffOn π•œ m f s :=
  ⟨fun H _ hm => H.of_le (mod_cast hm), fun H x hx m hm => H m hm x hx m le_rfl⟩
Characterization of $C^n$ Differentiability on a Set via Finite Orders
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any extended natural number $n \in \mathbb{N}_\infty$ and any subset $s \subseteq E$, the function $f$ is $C^n$ on $s$ if and only if for every natural number $m \in \mathbb{N}$ such that $m \leq n$, the function $f$ is $C^m$ on $s$.
contDiffOn_infty theorem
: ContDiffOn π•œ ∞ f s ↔ βˆ€ n : β„•, ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_infty : ContDiffOnContDiffOn π•œ ∞ f s ↔ βˆ€ n : β„•, ContDiffOn π•œ n f s :=
  contDiffOn_iff_forall_nat_le.trans <| by simp only [le_top, forall_prop_of_true]
Characterization of $C^\infty$ Differentiability on a Set via Finite Orders
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^\infty$ on a set $s \subseteq E$ (i.e., $\text{ContDiffOn}\ \mathbb{K}\ \infty\ f\ s$) if and only if for every natural number $n \in \mathbb{N}$, the function $f$ is $C^n$ on $s$ (i.e., $\text{ContDiffOn}\ \mathbb{K}\ n\ f\ s$).
contDiffOn_all_iff_nat theorem
: (βˆ€ (n : β„•βˆž), ContDiffOn π•œ n f s) ↔ βˆ€ n : β„•, ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_all_iff_nat :
    (βˆ€ (n : β„•βˆž), ContDiffOn π•œ n f s) ↔ βˆ€ n : β„•, ContDiffOn π•œ n f s := by
  refine ⟨fun H n => H n, ?_⟩
  rintro H (_ | n)
  exacts [contDiffOn_infty.2 H, H n]
Characterization of Infinite Differentiability via Finite Orders on a Set
Informal description
For a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ and a subset $s \subseteq E$, the following are equivalent: 1. $f$ is $C^n$ on $s$ for all extended natural numbers $n \in \mathbb{N}_\infty$. 2. $f$ is $C^n$ on $s$ for all natural numbers $n \in \mathbb{N}$.
ContDiffOn.continuousOn theorem
(h : ContDiffOn π•œ n f s) : ContinuousOn f s
Full source 
theorem ContDiffOn.continuousOn (h : ContDiffOn π•œ n f s) : ContinuousOn f s := fun x hx =>
  (h x hx).continuousWithinAt
Continuity of \( C^n \) Functions on a Set
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^n \) on a set \( s \subseteq E \) (i.e., \( f \) has continuous derivatives up to order \( n \) in a neighborhood of each point \( x \in s \) within \( s \cup \{x\} \)), then \( f \) is continuous on \( s \).
ContDiffOn.congr theorem
(h : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s, f₁ x = f x) : ContDiffOn π•œ n f₁ s
Full source 
theorem ContDiffOn.congr (h : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s, f₁ x = f x) :
    ContDiffOn π•œ n f₁ s := fun x hx => (h x hx).congr h₁ (h₁ x hx)
Preservation of $C^n$ Differentiability on a Set under Pointwise Equality
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If $f : E \to F$ is $C^n$ on $s$ and $f_1 : E \to F$ satisfies $f_1(x) = f(x)$ for all $x \in s$, then $f_1$ is also $C^n$ on $s$.
contDiffOn_congr theorem
(h₁ : βˆ€ x ∈ s, f₁ x = f x) : ContDiffOn π•œ n f₁ s ↔ ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_congr (h₁ : βˆ€ x ∈ s, f₁ x = f x) : ContDiffOnContDiffOn π•œ n f₁ s ↔ ContDiffOn π•œ n f s :=
  ⟨fun H => H.congr fun x hx => (h₁ x hx).symm, fun H => H.congr hβ‚βŸ©
Equivalence of $C^n$ Differentiability for Pointwise Equal Functions on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. For two functions $f, f_1 : E \to F$ such that $f_1(x) = f(x)$ for all $x \in s$, the function $f_1$ is $C^n$ on $s$ if and only if $f$ is $C^n$ on $s$.
ContDiffOn.mono theorem
(h : ContDiffOn π•œ n f s) {t : Set E} (hst : t βŠ† s) : ContDiffOn π•œ n f t
Full source 
theorem ContDiffOn.mono (h : ContDiffOn π•œ n f s) {t : Set E} (hst : t βŠ† s) : ContDiffOn π•œ n f t :=
  fun x hx => (h x (hst hx)).mono hst
$C^n$ Differentiability is Preserved Under Subset Restriction
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ on a set $s \subseteq E$, then for any subset $t \subseteq s$, the function $f$ is also $C^n$ on $t$.
ContDiffOn.congr_mono theorem
(hf : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s₁, f₁ x = f x) (hs : s₁ βŠ† s) : ContDiffOn π•œ n f₁ s₁
Full source 
theorem ContDiffOn.congr_mono (hf : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s₁, f₁ x = f x) (hs : s₁ βŠ† s) :
    ContDiffOn π•œ n f₁ s₁ :=
  (hf.mono hs).congr h₁
Preservation of $C^n$ Differentiability Under Pointwise Equality and Subset Restriction
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s, s_1 \subseteq E$ with $s_1 \subseteq s$. If $f : E \to F$ is $C^n$ on $s$ and $f_1 : E \to F$ satisfies $f_1(x) = f(x)$ for all $x \in s_1$, then $f_1$ is $C^n$ on $s_1$.
ContDiffOn.differentiableOn theorem
(h : ContDiffOn π•œ n f s) (hn : 1 ≀ n) : DifferentiableOn π•œ f s
Full source 
/-- If a function is `C^n` on a set with `n β‰₯ 1`, then it is differentiable there. -/
theorem ContDiffOn.differentiableOn (h : ContDiffOn π•œ n f s) (hn : 1 ≀ n) :
    DifferentiableOn π•œ f s := fun x hx => (h x hx).differentiableWithinAt hn
Differentiability of $C^n$ Functions on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If a function $f : E \to F$ is $C^n$ on $s$ for some $n \geq 1$, then $f$ is differentiable on $s$.
contDiffOn_of_locally_contDiffOn theorem
(h : βˆ€ x ∈ s, βˆƒ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ n f (s ∩ u)) : ContDiffOn π•œ n f s
Full source 
/-- If a function is `C^n` around each point in a set, then it is `C^n` on the set. -/
theorem contDiffOn_of_locally_contDiffOn
    (h : βˆ€ x ∈ s, βˆƒ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ n f (s ∩ u)) : ContDiffOn π•œ n f s := by
  intro x xs
  rcases h x xs with ⟨u, u_open, xu, hu⟩
  apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)
  exact IsOpen.mem_nhds u_open xu
Local $C^n$ Differentiability Implies Global $C^n$ Differentiability on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If for every point $x \in s$ there exists an open neighborhood $u$ of $x$ such that the function $f : E \to F$ is $C^n$ on $s \cap u$, then $f$ is $C^n$ on the entire set $s$.
contDiffOn_succ_iff_hasFDerivWithinAt theorem
(hn : n β‰  ∞) : ContDiffOn π•œ (n + 1) f s ↔ βˆ€ x ∈ s, βˆƒ u ∈ 𝓝[insert x s] x, (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧ βˆƒ f' : E β†’ E β†’L[π•œ] F, (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn π•œ n f' u
Full source 
/-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`. -/
theorem contDiffOn_succ_iff_hasFDerivWithinAt (hn : n β‰  ∞) :
    ContDiffOnContDiffOn π•œ (n + 1) f s ↔
      βˆ€ x ∈ s, βˆƒ u ∈ 𝓝[insert x s] x, (n = Ο‰ β†’ AnalyticOn π•œ f u) ∧ βˆƒ f' : E β†’ E β†’L[π•œ] F,
        (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn π•œ n f' u := by
  constructor
  Β· intro h x hx
    rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).1 (h x hx) with
      ⟨u, hu, f_an, f', hf', Hf'⟩
    rcases Hf'.contDiffOn le_rfl (by simp [hn]) with ⟨v, vu, v'u, hv⟩
    rw [insert_eq_of_mem hx] at hu ⊒
    have xu : x ∈ u := mem_of_mem_nhdsWithin hx hu
    rw [insert_eq_of_mem xu] at vu v'u
    exact ⟨v, nhdsWithin_le_of_mem hu vu, fun h ↦ (f_an h).mono v'u, f',
      fun y hy ↦ (hf' y (v'u hy)).mono v'u, hv⟩
  Β· intro h x hx
    rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn]
    rcases h x hx with ⟨u, u_nhbd, f_an, f', hu, hf'⟩
    have : x ∈ u := mem_of_mem_nhdsWithin (mem_insert _ _) u_nhbd
    exact ⟨u, u_nhbd, f_an, f', hu, hf' x this⟩
Characterization of $C^{n+1}$ Differentiability via Local Existence of $C^n$ Derivative on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $n \in \mathbb{N}_\infty$ with $n \neq \infty$. Then the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ on $s$. 2. For every $x \in s$, there exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ such that: - If $n = \omega$, then $f$ is analytic on $u$. - There exists a derivative function $f' : E \to (E \toL[\mathbb{K}] F)$ such that: * For all $y \in u$, $f$ has FrΓ©chet derivative $f'(y)$ within $u$ at $y$. * $f'$ is $C^n$ on $u$.
contDiffOn_zero theorem
: ContDiffOn π•œ 0 f s ↔ ContinuousOn f s
Full source 
@[simp]
theorem contDiffOn_zero : ContDiffOnContDiffOn π•œ 0 f s ↔ ContinuousOn f s := by
  refine ⟨fun H => H.continuousOn, fun H => fun x hx m hm ↦ ?_⟩
  have : (m : WithTop β„•βˆž) = 0 := le_antisymm (mod_cast hm) bot_le
  rw [this]
  refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin π•œ f s, ?_⟩
  rw [hasFTaylorSeriesUpToOn_zero_iff]
  exact ⟨by rwa [insert_eq_of_mem hx], fun x _ => by simp [ftaylorSeriesWithin]⟩
$C^0$ Differentiability is Equivalent to Continuity on a Set
Informal description
A function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^0$ on a set $s \subseteq E$ if and only if $f$ is continuous on $s$.
contDiffWithinAt_zero theorem
(hx : x ∈ s) : ContDiffWithinAt π•œ 0 f s x ↔ βˆƒ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)
Full source 
theorem contDiffWithinAt_zero (hx : x ∈ s) :
    ContDiffWithinAtContDiffWithinAt π•œ 0 f s x ↔ βˆƒ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u) := by
  constructor
  Β· intro h
    obtain ⟨u, H, p, hp⟩ := h 0 le_rfl
    refine ⟨u, ?_, ?_⟩
    Β· simpa [hx] using H
    Β· simp only [Nat.cast_zero, hasFTaylorSeriesUpToOn_zero_iff] at hp
      exact hp.1.mono inter_subset_right
  · rintro ⟨u, H, hu⟩
    rw [← contDiffWithinAt_inter' H]
    have h' : x ∈ s ∩ u := ⟨hx, mem_of_mem_nhdsWithin hx H⟩
    exact (contDiffOn_zero.mpr hu).contDiffWithinAt h'
Characterization of \( C^0 \) Differentiability Within a Set at a Point
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), a point \( x \in s \subseteq E \), and \( n = 0 \), the following are equivalent: 1. \( f \) is \( C^0 \) within \( s \) at \( x \) (i.e., \( \text{ContDiffWithinAt}\, \mathbb{K}\, 0\, f\, s\, x \) holds). 2. There exists a neighborhood \( u \) of \( x \) within \( s \) such that \( f \) is continuous on \( s \cap u \).
ContDiffOn.ftaylorSeriesWithin theorem
(h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) : HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin π•œ f s) s
Full source 
/-- When a function is `C^n` in a set `s` of unique differentiability, it admits
`ftaylorSeriesWithin π•œ f s` as a Taylor series up to order `n` in `s`. -/
protected theorem ContDiffOn.ftaylorSeriesWithin
    (h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) :
    HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin π•œ f s) s := by
  constructor
  Β· intro x _
    simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
      iteratedFDerivWithin_zero_apply]
  Β· intro m hm x hx
    have : (m + 1 : β„•) ≀ n := ENat.add_one_natCast_le_withTop_of_lt hm
    rcases (h x hx).of_le this _ le_rfl with ⟨u, hu, p, Hp⟩
    rw [insert_eq_of_mem hx] at hu
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [inter_comm] at ho
    have : p x m.succ = ftaylorSeriesWithin π•œ f s x m.succ := by
      change p x m.succ = iteratedFDerivWithin π•œ m.succ f s x
      rw [← iteratedFDerivWithin_inter_open o_open xo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
    rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]
    have A : βˆ€ y ∈ s ∩ o, p y m = ftaylorSeriesWithin π•œ f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin π•œ m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact
        (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m)
          (hs.inter o_open) ⟨hy, yo⟩
    exact
      ((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr
        (fun y hy => (A y hy).symm) (A x ⟨hx, xo⟩).symm
  Β· intro m hm
    apply continuousOn_of_locally_continuousOn
    intro x hx
    rcases (h x hx).of_le hm _ le_rfl with ⟨u, hu, p, Hp⟩
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [insert_eq_of_mem hx] at ho
    rw [inter_comm] at ho
    refine ⟨o, o_open, xo, ?_⟩
    have A : βˆ€ y ∈ s ∩ o, p y m = ftaylorSeriesWithin π•œ f s y m := by
      rintro y ⟨hy, yo⟩
      change p y m = iteratedFDerivWithin π•œ m f s y
      rw [← iteratedFDerivWithin_inter_open o_open yo]
      exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩
    exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm
Existence of Taylor Series for $C^n$ Functions on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ on a set $s \subseteq E$ (i.e., $f$ is $n$-times continuously differentiable on $s$). If $s$ has the property of unique differentiability (meaning the derivatives of functions on $s$ are uniquely determined), then the function $f$ admits the formal Taylor series $\text{ftaylorSeriesWithin}\, \mathbb{K}\, f\, s$ as a valid Taylor series expansion up to order $n$ on $s$.
iteratedFDerivWithin_subset theorem
{n : β„•} (st : s βŠ† t) (hs : UniqueDiffOn π•œ s) (ht : UniqueDiffOn π•œ t) (h : ContDiffOn π•œ n f t) (hx : x ∈ s) : iteratedFDerivWithin π•œ n f s x = iteratedFDerivWithin π•œ n f t x
Full source 
theorem iteratedFDerivWithin_subset {n : β„•} (st : s βŠ† t) (hs : UniqueDiffOn π•œ s)
    (ht : UniqueDiffOn π•œ t) (h : ContDiffOn π•œ n f t) (hx : x ∈ s) :
    iteratedFDerivWithin π•œ n f s x = iteratedFDerivWithin π•œ n f t x :=
  (((h.ftaylorSeriesWithin ht).mono st).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hs hx).symm
Agreement of Iterated Derivatives on Subsets with Unique Differentiability
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function that is \( C^n \) on a set \( t \subseteq E \). Suppose \( s \subseteq t \) and both \( s \) and \( t \) have the property of unique differentiability. Then, for any \( x \in s \), the \( n \)-th iterated derivative of \( f \) within \( s \) at \( x \) coincides with the \( n \)-th iterated derivative of \( f \) within \( t \) at \( x \).
ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn theorem
{f : E β†’ F} {s : Set E} {a : E} (h : ContDiffWithinAt π•œ n f s a) (hs : UniqueDiffOn π•œ s) (ha : a ∈ s) {m : β„•} (hm : m ≀ n) : βˆ€αΆ  t in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn m f (ftaylorSeriesWithin π•œ f s) t
Full source 
theorem ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn {f : E β†’ F} {s : Set E} {a : E}
    (h : ContDiffWithinAt π•œ n f s a) (hs : UniqueDiffOn π•œ s) (ha : a ∈ s) {m : β„•} (hm : m ≀ n) :
    βˆ€αΆ  t in (𝓝[s] a).smallSets, HasFTaylorSeriesUpToOn m f (ftaylorSeriesWithin π•œ f s) t := by
  rcases h.contDiffOn' hm (by simp) with ⟨U, hUo, haU, hfU⟩
  have : βˆ€αΆ  t in (𝓝[s] a).smallSets, t βŠ† s ∩ U := by
    rw [eventually_smallSets_subset]
    exact inter_mem_nhdsWithin _ <| hUo.mem_nhds haU
  refine this.mono fun t ht ↦ .mono ?_ ht
  rw [insert_eq_of_mem ha] at hfU
  refine (hfU.ftaylorSeriesWithin (hs.inter hUo)).congr_series fun k hk x hx ↦ ?_
  exact iteratedFDerivWithin_inter_open hUo hx.2
Local existence of Taylor series for $C^n$ functions on uniquely differentiable sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ within a set $s \subseteq E$ at a point $a \in s$. If $s$ has the property of unique differentiability, then for any natural number $m \leq n$, there exists a neighborhood $t$ of $a$ within $s$ such that $f$ has a Taylor series up to order $m$ on $t$ with coefficients given by the formal Taylor series $\text{ftaylorSeriesWithin}\, \mathbb{K}\, f\, s$.
AnalyticOn.contDiffOn theorem
(h : AnalyticOn π•œ f s) (hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ n f s
Full source 
/-- On a set with unique differentiability, an analytic function is automatically `C^Ο‰`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOn.contDiffOn_of_completeSpace`. -/
theorem AnalyticOn.contDiffOn (h : AnalyticOn π•œ f s) (hs : UniqueDiffOn π•œ s) :
    ContDiffOn π•œ n f s := by
  suffices ContDiffOn π•œ Ο‰ f s from this.of_le le_top
  rcases h.exists_hasFTaylorSeriesUpToOn hs with ⟨p, hp⟩
  intro x hx
  refine ⟨s, ?_, p, hp⟩
  rw [insert_eq_of_mem hx]
  exact self_mem_nhdsWithin
Analytic Functions on Uniquely Differentiable Sets are $C^n$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is analytic on a set $s \subseteq E$. If $s$ has the property of unique differentiability (i.e., the FrΓ©chet derivative is uniquely determined at each point in $s$), then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
AnalyticOnNhd.contDiffOn theorem
(h : AnalyticOnNhd π•œ f s) (hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ n f s
Full source 
/-- On a set with unique differentiability, an analytic function is automatically `C^Ο‰`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOnNhd.contDiffOn_of_completeSpace`. -/
theorem AnalyticOnNhd.contDiffOn (h : AnalyticOnNhd π•œ f s) (hs : UniqueDiffOn π•œ s) :
    ContDiffOn π•œ n f s := h.analyticOn.contDiffOn hs
Analyticity on a neighborhood implies $C^n$ differentiability on uniquely differentiable sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is analytic on a neighborhood of a set $s \subseteq E$. If $s$ has the property of unique differentiability (i.e., the FrΓ©chet derivative is uniquely determined at each point in $s$), then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
AnalyticOn.contDiffOn_of_completeSpace theorem
[CompleteSpace F] (h : AnalyticOn π•œ f s) : ContDiffOn π•œ n f s
Full source 
/-- An analytic function is automatically `C^Ο‰` in a complete space -/
theorem AnalyticOn.contDiffOn_of_completeSpace [CompleteSpace F] (h : AnalyticOn π•œ f s) :
    ContDiffOn π•œ n f s :=
  fun x hx ↦ (h x hx).contDiffWithinAt
Analyticity implies $C^n$ differentiability in complete spaces
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $F$ complete. If a function $f : E \to F$ is analytic on a set $s \subseteq E$, then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
AnalyticOnNhd.contDiffOn_of_completeSpace theorem
[CompleteSpace F] (h : AnalyticOnNhd π•œ f s) : ContDiffOn π•œ n f s
Full source 
/-- An analytic function is automatically `C^Ο‰` in a complete space -/
theorem AnalyticOnNhd.contDiffOn_of_completeSpace [CompleteSpace F] (h : AnalyticOnNhd π•œ f s) :
    ContDiffOn π•œ n f s :=
  h.analyticOn.contDiffOn_of_completeSpace
Analyticity on neighborhood implies $C^n$ differentiability in complete spaces
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $F$ complete. If a function $f : E \to F$ is analytic on a neighborhood of a set $s \subseteq E$, then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
contDiffOn_of_continuousOn_differentiableOn theorem
{n : β„•βˆž} (Hcont : βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s) (Hdiff : βˆ€ m : β„•, m < n β†’ DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s) : ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_of_continuousOn_differentiableOn {n : β„•βˆž}
    (Hcont : βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s)
    (Hdiff : βˆ€ m : β„•, m < n β†’
      DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s) :
    ContDiffOn π•œ n f s := by
  intro x hx m hm
  rw [insert_eq_of_mem hx]
  refine ⟨s, self_mem_nhdsWithin, ftaylorSeriesWithin π•œ f s, ?_⟩
  constructor
  Β· intro y _
    simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
      iteratedFDerivWithin_zero_apply]
  Β· intro k hk y hy
    convert (Hdiff k (lt_of_lt_of_le (mod_cast hk) (mod_cast hm)) y hy).hasFDerivWithinAt
  Β· intro k hk
    exact Hcont k (le_trans (mod_cast hk) (mod_cast hm))
Sufficient Conditions for $C^n$ Differentiability on a Set via Continuous and Differentiable Iterated Derivatives
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function defined on a set $s \subseteq E$. For an extended natural number $n \in \mathbb{N}_\infty$, if for every natural number $m \leq n$ the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^m f s$ is continuous on $s$, and for every $m < n$ the $m$-th iterated FrΓ©chet derivative is differentiable on $s$, then $f$ is $C^n$ on $s$.
contDiffOn_of_differentiableOn theorem
{n : β„•βˆž} (h : βˆ€ m : β„•, m ≀ n β†’ DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s) : ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_of_differentiableOn {n : β„•βˆž}
    (h : βˆ€ m : β„•, m ≀ n β†’ DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s) :
    ContDiffOn π•œ n f s :=
  contDiffOn_of_continuousOn_differentiableOn (fun m hm => (h m hm).continuousOn) fun m hm =>
    h m (le_of_lt hm)
Differentiability of Iterated Derivatives Implies $C^n$ Differentiability on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function defined on a set $s \subseteq E$. For an extended natural number $n \in \mathbb{N}_\infty$, if for every natural number $m \leq n$ the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^m f s$ is differentiable on $s$, then $f$ is $C^n$ on $s$.
contDiffOn_of_analyticOn_iteratedFDerivWithin theorem
(h : βˆ€ m, AnalyticOn π•œ (iteratedFDerivWithin π•œ m f s) s) : ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_of_analyticOn_iteratedFDerivWithin
    (h : βˆ€ m, AnalyticOn π•œ (iteratedFDerivWithin π•œ m f s) s) :
    ContDiffOn π•œ n f s := by
  suffices ContDiffOn π•œ Ο‰ f s from this.of_le le_top
  intro x hx
  refine ⟨insert x s, self_mem_nhdsWithin, ftaylorSeriesWithin π•œ f s, ?_, ?_⟩
  Β· rw [insert_eq_of_mem hx]
    constructor
    Β· intro y _
      simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
        iteratedFDerivWithin_zero_apply]
    Β· intro k _ y hy
      exact ((h k).differentiableOn y hy).hasFDerivWithinAt
    Β· intro k _
      exact (h k).continuousOn
  Β· intro i
    rw [insert_eq_of_mem hx]
    exact h i
Analyticity of Iterated Derivatives Implies $C^n$ Differentiability on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function defined on a set $s \subseteq E$. If for every natural number $m$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^m f s$ is analytic on $s$, then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
contDiffOn_omega_iff_analyticOn theorem
(hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ Ο‰ f s ↔ AnalyticOn π•œ f s
Full source 
theorem contDiffOn_omega_iff_analyticOn (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ Ο‰ f s ↔ AnalyticOn π•œ f s :=
  ⟨fun h m ↦ h.analyticOn m, fun h ↦ h.contDiffOn hs⟩
Equivalence of $C^\omega$ and Analyticity on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function defined on a set $s \subseteq E$. If $s$ has the property of unique differentiability, then $f$ is $C^\omega$ (analytic) on $s$ if and only if $f$ is analytic on $s$.
ContDiffOn.continuousOn_iteratedFDerivWithin theorem
{m : β„•} (h : ContDiffOn π•œ n f s) (hmn : m ≀ n) (hs : UniqueDiffOn π•œ s) : ContinuousOn (iteratedFDerivWithin π•œ m f s) s
Full source 
theorem ContDiffOn.continuousOn_iteratedFDerivWithin {m : β„•} (h : ContDiffOn π•œ n f s)
    (hmn : m ≀ n) (hs : UniqueDiffOn π•œ s) : ContinuousOn (iteratedFDerivWithin π•œ m f s) s :=
  ((h.of_le hmn).ftaylorSeriesWithin hs).cont m le_rfl
Continuity of Iterated Derivatives for $C^n$ Functions on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ on a set $s \subseteq E$. If $s$ has the property of unique differentiability and $m$ is a natural number with $m \leq n$, then the $m$-th iterated FrΓ©chet derivative of $f$ within $s$, denoted $\text{iteratedFDerivWithin}\, \mathbb{K}\, m\, f\, s$, is continuous on $s$.
ContDiffOn.differentiableOn_iteratedFDerivWithin theorem
{m : β„•} (h : ContDiffOn π•œ n f s) (hmn : m < n) (hs : UniqueDiffOn π•œ s) : DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s
Full source 
theorem ContDiffOn.differentiableOn_iteratedFDerivWithin {m : β„•} (h : ContDiffOn π•œ n f s)
    (hmn : m < n) (hs : UniqueDiffOn π•œ s) :
    DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s := by
  intro x hx
  have : (m + 1 : β„•) ≀ n := ENat.add_one_natCast_le_withTop_of_lt hmn
  apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt
  exact_mod_cast lt_add_one m
Differentiability of Iterated Derivatives for $C^n$ Functions on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ on a set $s \subseteq E$. If $m$ is a natural number with $m < n$ and $s$ has the property of unique differentiability, then the $m$-th iterated FrΓ©chet derivative of $f$ within $s$ is differentiable on $s$.
ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin theorem
{m : β„•} (h : ContDiffWithinAt π•œ n f s x) (hmn : m < n) (hs : UniqueDiffOn π•œ (insert x s)) : DifferentiableWithinAt π•œ (iteratedFDerivWithin π•œ m f s) s x
Full source 
theorem ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin {m : β„•}
    (h : ContDiffWithinAt π•œ n f s x) (hmn : m < n) (hs : UniqueDiffOn π•œ (insert x s)) :
    DifferentiableWithinAt π•œ (iteratedFDerivWithin π•œ m f s) s x := by
  have : (m + 1 : WithTop β„•βˆž) β‰  ∞ := Ne.symm (ne_of_beq_false rfl)
  rcases h.contDiffOn' (ENat.add_one_natCast_le_withTop_of_lt hmn) (by simp [this])
    with ⟨u, uo, xu, hu⟩
  set t := insert x s ∩ u
  have A : t =αΆ [𝓝[β‰ ] x] s := by
    simp only [set_eventuallyEq_iff_inf_principal, ← nhdsWithin_inter']
    rw [← inter_assoc, nhdsWithin_inter_of_mem', ← diff_eq_compl_inter, insert_diff_of_mem,
      diff_eq_compl_inter]
    exacts [rfl, mem_nhdsWithin_of_mem_nhds (uo.mem_nhds xu)]
  have B : iteratedFDerivWithiniteratedFDerivWithin π•œ m f s =αΆ [𝓝 x] iteratedFDerivWithin π•œ m f t :=
    iteratedFDerivWithin_eventually_congr_set' _ A.symm _
  have C : DifferentiableWithinAt π•œ (iteratedFDerivWithin π•œ m f t) t x :=
    hu.differentiableOn_iteratedFDerivWithin (Nat.cast_lt.2 m.lt_succ_self) (hs.inter uo) x
      ⟨mem_insert _ _, xu⟩
  rw [differentiableWithinAt_congr_set' _ A] at C
  exact C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds
Differentiability of Iterated Derivatives for $C^n$ Functions at a Point in Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $x \in E$ a point. If $f : E \to F$ is $C^n$ within $s$ at $x$, and if $m < n$ is a natural number, and if the set $s \cup \{x\}$ has the property of unique differentiability, then the $m$-th iterated FrΓ©chet derivative of $f$ within $s$ is differentiable within $s$ at $x$.
contDiffOn_iff_continuousOn_differentiableOn theorem
{n : β„•βˆž} (hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ n f s ↔ (βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s) ∧ βˆ€ m : β„•, m < n β†’ DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s
Full source 
theorem contDiffOn_iff_continuousOn_differentiableOn {n : β„•βˆž} (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ n f s ↔
      (βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s) ∧
        βˆ€ m : β„•, m < n β†’ DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s :=
  ⟨fun h => ⟨fun _m hm => h.continuousOn_iteratedFDerivWithin (mod_cast hm) hs,
      fun _m hm => h.differentiableOn_iteratedFDerivWithin (mod_cast hm) hs⟩,
    fun h => contDiffOn_of_continuousOn_differentiableOn h.1 h.2⟩
Characterization of $C^n$ Differentiability on Uniquely Differentiable Sets via Iterated Derivatives
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with the property of unique differentiability. For an extended natural number $n \in \mathbb{N}_\infty$, a function $f : E \to F$ is $C^n$ on $s$ if and only if for every natural number $m \leq n$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^m f s$ is continuous on $s$, and for every $m < n$, the $m$-th iterated FrΓ©chet derivative is differentiable on $s$.
contDiffOn_nat_iff_continuousOn_differentiableOn theorem
{n : β„•} (hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ n f s ↔ (βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s) ∧ βˆ€ m : β„•, m < n β†’ DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s
Full source 
theorem contDiffOn_nat_iff_continuousOn_differentiableOn {n : β„•} (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ n f s ↔
      (βˆ€ m : β„•, m ≀ n β†’ ContinuousOn (fun x => iteratedFDerivWithin π•œ m f s x) s) ∧
        βˆ€ m : β„•, m < n β†’ DifferentiableOn π•œ (fun x => iteratedFDerivWithin π•œ m f s x) s := by
  rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]
  simp
Characterization of $C^n$ Differentiability on Uniquely Differentiable Sets via Iterated Derivatives (Finite Case)
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a set with the property of unique differentiability. For a natural number $n \in \mathbb{N}$, a function $f : E \to F$ is $C^n$ on $s$ if and only if for every natural number $m \leq n$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^m f s$ is continuous on $s$, and for every $m < n$, the $m$-th iterated FrΓ©chet derivative is differentiable on $s$.
contDiffOn_succ_of_fderivWithin theorem
(hf : DifferentiableOn π•œ f s) (h' : n = Ο‰ β†’ AnalyticOn π•œ f s) (h : ContDiffOn π•œ n (fun y => fderivWithin π•œ f s y) s) : ContDiffOn π•œ (n + 1) f s
Full source 
theorem contDiffOn_succ_of_fderivWithin (hf : DifferentiableOn π•œ f s)
    (h' : n = Ο‰ β†’ AnalyticOn π•œ f s)
    (h : ContDiffOn π•œ n (fun y => fderivWithin π•œ f s y) s) : ContDiffOn π•œ (n + 1) f s := by
  rcases eq_or_ne n ∞ with rfl | hn
  Β· rw [ENat.coe_top_add_one, contDiffOn_infty]
    intro m x hx
    apply ContDiffWithinAt.of_le _ (show (m : WithTop β„•βˆž) ≀ m + 1 from le_self_add)
    rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp),
      insert_eq_of_mem hx]
    exact ⟨s, self_mem_nhdsWithin, (by simp), fderivWithin π•œ f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, (h x hx).of_le (mod_cast le_top)⟩
  Β· intro x hx
    rw [contDiffWithinAt_succ_iff_hasFDerivWithinAt hn,
      insert_eq_of_mem hx]
    exact ⟨s, self_mem_nhdsWithin, h', fderivWithin π•œ f s,
      fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩
$C^{n+1}$ Differentiability via $C^n$ Differentiability of the FrΓ©chet Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose $f : E \to F$ is differentiable on $s$ (i.e., $\text{DifferentiableOn}\ \mathbb{K}\ f\ s$), and for $n = \omega$ (the analytic case), $f$ is analytic on $s$. If the FrΓ©chet derivative of $f$ within $s$, denoted $y \mapsto \text{fderivWithin}\ \mathbb{K}\ f\ s\ y$, is $C^n$ on $s$, then $f$ is $C^{n+1}$ on $s$.
contDiffOn_of_analyticOn_of_fderivWithin theorem
(hf : AnalyticOn π•œ f s) (h : ContDiffOn π•œ Ο‰ (fun y ↦ fderivWithin π•œ f s y) s) : ContDiffOn π•œ n f s
Full source 
theorem contDiffOn_of_analyticOn_of_fderivWithin (hf : AnalyticOn π•œ f s)
    (h : ContDiffOn π•œ Ο‰ (fun y ↦ fderivWithin π•œ f s y) s) : ContDiffOn π•œ n f s := by
  suffices ContDiffOn π•œ (Ο‰ + 1) f s from this.of_le le_top
  exact contDiffOn_succ_of_fderivWithin hf.differentiableOn (fun _ ↦ hf) h
Analyticity and Analytic Derivative Imply $C^n$ Differentiability
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If a function $f : E \to F$ is analytic on $s$ and its FrΓ©chet derivative within $s$ (i.e., the function $y \mapsto \text{fderivWithin}_{\mathbb{K}} f s y$) is $C^\omega$ (analytic) on $s$, then $f$ is $C^n$ on $s$ for any extended natural number $n \in \mathbb{N}_\infty$.
contDiffOn_succ_iff_fderivWithin theorem
(hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ (n + 1) f s ↔ DifferentiableOn π•œ f s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧ ContDiffOn π•œ n (fderivWithin π•œ f s) s
Full source 
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is
differentiable there, and its derivative (expressed with `fderivWithin`) is `C^n`. -/
theorem contDiffOn_succ_iff_fderivWithin (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ (n + 1) f s ↔
      DifferentiableOn π•œ f s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧
      ContDiffOn π•œ n (fderivWithin π•œ f s) s := by
  refine ⟨fun H => ?_, fun h => contDiffOn_succ_of_fderivWithin h.1 h.2.1 h.2.2⟩
  refine ⟨H.differentiableOn le_add_self, ?_, fun x hx => ?_⟩
  Β· rintro rfl
    exact H.analyticOn
  have A (m : β„•) (hm : m ≀ n) : ContDiffWithinAt π•œ m (fun y => fderivWithin π•œ f s y) s x := by
    rcases (contDiffWithinAt_succ_iff_hasFDerivWithinAt (n := m) (ne_of_beq_false rfl)).1
      (H.of_le (add_le_add_right hm 1) x hx) with ⟨u, hu, -, f', hff', hf'⟩
    rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
    rw [inter_comm, insert_eq_of_mem hx] at ho
    have := hf'.mono ho
    rw [contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds o_open xo))] at this
    apply this.congr_of_eventuallyEq_of_mem _ hx
    have : o ∩ so ∩ s ∈ 𝓝[s] x := mem_nhdsWithin.2 ⟨o, o_open, xo, Subset.refl _⟩
    rw [inter_comm] at this
    refine Filter.eventuallyEq_of_mem this fun y hy => ?_
    have A : fderivWithin π•œ f (s ∩ o) y = f' y :=
      ((hff' y (ho hy)).mono ho).fderivWithin (hs.inter o_open y hy)
    rwa [fderivWithin_inter (o_open.mem_nhds hy.2)] at A
  match n with
  | Ο‰ => exact (H.analyticOn.fderivWithin hs).contDiffOn hs (n := Ο‰) x hx
  | ∞ => exact contDiffWithinAt_infty.2 (fun m ↦ A m (mod_cast le_top))
  | (n : β„•) => exact A n le_rfl
Characterization of $C^{n+1}$ Differentiability via Differentiability and $C^n$ Differentiability of the Derivative on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with unique differentiability. For any extended natural number $n \in \mathbb{N}_\infty$, the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ on $s$. 2. The function $f$ is differentiable on $s$, and: - If $n = \omega$ (the analytic case), then $f$ is analytic on $s$. - The FrΓ©chet derivative of $f$ within $s$, denoted by $fderivWithin_{\mathbb{K}} f s$, is $C^n$ on $s$.
contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn theorem
(hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ (n + 1) f s ↔ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧ βˆƒ f' : E β†’ E β†’L[π•œ] F, ContDiffOn π•œ n f' s ∧ βˆ€ x, x ∈ s β†’ HasFDerivWithinAt f (f' x) s x
Full source 
theorem contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ (n + 1) f s ↔ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧
      βˆƒ f' : E β†’ E β†’L[π•œ] F, ContDiffOn π•œ n f' s ∧ βˆ€ x, x ∈ s β†’ HasFDerivWithinAt f (f' x) s x := by
  rw [contDiffOn_succ_iff_fderivWithin hs]
  refine ⟨fun h => ⟨h.2.1, fderivWithin π•œ f s, h.2.2,
    fun x hx => (h.1 x hx).hasFDerivWithinAt⟩, fun ⟨f_an, h⟩ => ?_⟩
  rcases h with ⟨f', h1, h2⟩
  refine ⟨fun x hx => (h2 x hx).differentiableWithinAt, f_an, fun x hx => ?_⟩
  exact (h1 x hx).congr_of_mem (fun y hy => (h2 y hy).fderivWithin (hs y hy)) hx
Characterization of $C^{n+1}$ Differentiability via Existence of $C^n$ Derivative on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with unique differentiability. For any extended natural number $n \in \mathbb{N}_\infty$, the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ on $s$. 2. The following conditions hold: - If $n = \omega$ (the analytic case), then $f$ is analytic on $s$. - There exists a function $f' : E \to E \toL[\mathbb{K}] F$ such that: - $f'$ is $C^n$ on $s$. - For every $x \in s$, $f$ has FrΓ©chet derivative $f'(x)$ within $s$ at $x$.
contDiffOn_infty_iff_fderivWithin theorem
(hs : UniqueDiffOn π•œ s) : ContDiffOn π•œ ∞ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ∞ (fderivWithin π•œ f s) s
Full source 
theorem contDiffOn_infty_iff_fderivWithin (hs : UniqueDiffOn π•œ s) :
    ContDiffOnContDiffOn π•œ ∞ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ∞ (fderivWithin π•œ f s) s := by
  rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderivWithin hs]
  simp
Characterization of $C^\infty$ Differentiability via Differentiability and $C^\infty$ Differentiability of the Derivative on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with unique differentiability. A function $f : E \to F$ is $C^\infty$ on $s$ if and only if: 1. $f$ is differentiable on $s$, and 2. The FrΓ©chet derivative of $f$ within $s$, denoted by $\text{fderivWithin}_{\mathbb{K}} f s$, is $C^\infty$ on $s$.
contDiffOn_succ_iff_fderiv_of_isOpen theorem
(hs : IsOpen s) : ContDiffOn π•œ (n + 1) f s ↔ DifferentiableOn π•œ f s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧ ContDiffOn π•œ n (fderiv π•œ f) s
Full source 
/-- A function is `C^(n + 1)` on an open domain if and only if it is
differentiable there, and its derivative (expressed with `fderiv`) is `C^n`. -/
theorem contDiffOn_succ_iff_fderiv_of_isOpen (hs : IsOpen s) :
    ContDiffOnContDiffOn π•œ (n + 1) f s ↔
      DifferentiableOn π•œ f s ∧ (n = Ο‰ β†’ AnalyticOn π•œ f s) ∧
      ContDiffOn π•œ n (fderiv π•œ f) s := by
  rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
    contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]
Characterization of $C^{n+1}$ Differentiability via Differentiability and $C^n$ Differentiability of the Derivative on Open Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be an open subset. For any extended natural number $n \in \mathbb{N}_\infty$, the following are equivalent: 1. The function $f : E \to F$ is $C^{n+1}$ on $s$. 2. The function $f$ is differentiable on $s$, and: - If $n = \omega$ (the analytic case), then $f$ is analytic on $s$. - The FrΓ©chet derivative of $f$, denoted by $fderiv_{\mathbb{K}} f$, is $C^n$ on $s$.
contDiffOn_infty_iff_fderiv_of_isOpen theorem
(hs : IsOpen s) : ContDiffOn π•œ ∞ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ∞ (fderiv π•œ f) s
Full source 
theorem contDiffOn_infty_iff_fderiv_of_isOpen (hs : IsOpen s) :
    ContDiffOnContDiffOn π•œ ∞ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ∞ (fderiv π•œ f) s := by
  rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]
  simp
Characterization of $C^\infty$ Differentiability via Differentiability and $C^\infty$ Differentiability of the Derivative on Open Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be an open subset. A function $f : E \to F$ is $C^\infty$ on $s$ if and only if: 1. $f$ is differentiable on $s$, and 2. The FrΓ©chet derivative of $f$, denoted by $\text{fderiv}_{\mathbb{K}} f$, is $C^\infty$ on $s$.
ContDiffOn.fderivWithin theorem
(hf : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) (hmn : m + 1 ≀ n) : ContDiffOn π•œ m (fderivWithin π•œ f s) s
Full source 
protected theorem ContDiffOn.fderivWithin (hf : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s)
    (hmn : m + 1 ≀ n) : ContDiffOn π•œ m (fderivWithin π•œ f s) s :=
  ((contDiffOn_succ_iff_fderivWithin hs).1 (hf.of_le hmn)).2.2
Differentiability of FrΓ©chet Derivative within a Uniquely Differentiable Set for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with unique differentiability. If a function $f : E \to F$ is $C^n$ on $s$ and $m + 1 \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then the FrΓ©chet derivative of $f$ within $s$, denoted by $fderivWithin_{\mathbb{K}} f s$, is $C^m$ on $s$.
ContDiffOn.fderiv_of_isOpen theorem
(hf : ContDiffOn π•œ n f s) (hs : IsOpen s) (hmn : m + 1 ≀ n) : ContDiffOn π•œ m (fderiv π•œ f) s
Full source 
theorem ContDiffOn.fderiv_of_isOpen (hf : ContDiffOn π•œ n f s) (hs : IsOpen s) (hmn : m + 1 ≀ n) :
    ContDiffOn π•œ m (fderiv π•œ f) s :=
  (hf.fderivWithin hs.uniqueDiffOn hmn).congr fun _ hx => (fderivWithin_of_isOpen hs hx).symm
Differentiability of FrΓ©chet Derivative on Open Sets for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be an open subset. If a function $f : E \to F$ is $C^n$ on $s$ and $m + 1 \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then the FrΓ©chet derivative of $f$, denoted by $fderiv_{\mathbb{K}} f$, is $C^m$ on $s$.
ContDiffOn.continuousOn_fderivWithin theorem
(h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) (hn : 1 ≀ n) : ContinuousOn (fderivWithin π•œ f s) s
Full source 
theorem ContDiffOn.continuousOn_fderivWithin (h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s)
    (hn : 1 ≀ n) : ContinuousOn (fderivWithin π•œ f s) s :=
  ((contDiffOn_succ_iff_fderivWithin hs).1
    (h.of_le (show 0 + (1 : WithTop β„•βˆž) ≀ n from hn))).2.2.continuousOn
Continuity of the FrΓ©chet Derivative Within a Uniquely Differentiable Set for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ on a set $s \subseteq E$ with $n \geq 1$, and $s$ has unique differentiability, then the FrΓ©chet derivative of $f$ within $s$, denoted by $fderivWithin_{\mathbb{K}} f s$, is continuous on $s$.
ContDiffOn.continuousOn_fderiv_of_isOpen theorem
(h : ContDiffOn π•œ n f s) (hs : IsOpen s) (hn : 1 ≀ n) : ContinuousOn (fderiv π•œ f) s
Full source 
theorem ContDiffOn.continuousOn_fderiv_of_isOpen (h : ContDiffOn π•œ n f s) (hs : IsOpen s)
    (hn : 1 ≀ n) : ContinuousOn (fderiv π•œ f) s :=
  ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1
    (h.of_le (show 0 + (1 : WithTop β„•βˆž) ≀ n from hn))).2.2.continuousOn
Continuity of the FrΓ©chet Derivative for $C^n$ Functions on Open Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be an open subset. If a function $f : E \to F$ is $C^n$ on $s$ with $n \geq 1$, then the FrΓ©chet derivative of $f$, denoted by $fderiv_{\mathbb{K}} f$, is continuous on $s$.
ContDiffAt definition
(n : WithTop β„•βˆž) (f : E β†’ F) (x : E) : Prop
Full source 
/-- A function is continuously differentiable up to `n` at a point `x` if, for any integer `k ≀ n`,
there is a neighborhood of `x` where `f` admits derivatives up to order `n`, which are continuous.
-/
def ContDiffAt (n : WithTop β„•βˆž) (f : E β†’ F) (x : E) : Prop :=
  ContDiffWithinAt π•œ n f univ x
\( C^n \) differentiability at a point
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^n \) at a point \( x \in E \) if it is \( C^n \) within the entire space \( E \) at \( x \). This means that for any integer \( k \leq n \), there exists a neighborhood of \( x \) where \( f \) admits derivatives up to order \( n \), which are continuous.
contDiffWithinAt_univ theorem
: ContDiffWithinAt π•œ n f univ x ↔ ContDiffAt π•œ n f x
Full source 
theorem contDiffWithinAt_univ : ContDiffWithinAtContDiffWithinAt π•œ n f univ x ↔ ContDiffAt π•œ n f x :=
  Iff.rfl
Equivalence of \( C^n \) Differentiability Within Universal Set and at a Point
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and for any extended natural number \( n \), the following are equivalent: 1. \( f \) is \( C^n \) within the universal set \( \text{univ} = E \) at a point \( x \in E \). 2. \( f \) is \( C^n \) at the point \( x \).
contDiffAt_infty theorem
: ContDiffAt π•œ ∞ f x ↔ βˆ€ n : β„•, ContDiffAt π•œ n f x
Full source 
theorem contDiffAt_infty : ContDiffAtContDiffAt π•œ ∞ f x ↔ βˆ€ n : β„•, ContDiffAt π•œ n f x := by
  simp [← contDiffWithinAt_univ, contDiffWithinAt_infty]
Characterization of \( C^\infty \) Differentiability at a Point via Finite Differentiability
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^\infty \) at a point \( x \in E \) if and only if it is \( C^n \) at \( x \) for every natural number \( n \).
ContDiffAt.contDiffWithinAt theorem
(h : ContDiffAt π•œ n f x) : ContDiffWithinAt π•œ n f s x
Full source 
theorem ContDiffAt.contDiffWithinAt (h : ContDiffAt π•œ n f x) : ContDiffWithinAt π•œ n f s x :=
  h.mono (subset_univ _)
\( C^n \) Differentiability at a Point Implies \( C^n \) Differentiability Within Any Set at That Point
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^n \) at a point \( x \in E \), then \( f \) is \( C^n \) within any set \( s \subseteq E \) at \( x \).
ContDiffWithinAt.contDiffAt theorem
(h : ContDiffWithinAt π•œ n f s x) (hx : s ∈ 𝓝 x) : ContDiffAt π•œ n f x
Full source 
theorem ContDiffWithinAt.contDiffAt (h : ContDiffWithinAt π•œ n f s x) (hx : s ∈ 𝓝 x) :
    ContDiffAt π•œ n f x := by rwa [ContDiffAt, ← contDiffWithinAt_inter hx, univ_inter]
$C^n$ Differentiability Within a Neighborhood Implies $C^n$ Differentiability at the Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ within a set $s \subseteq E$ at a point $x \in E$, and $s$ is a neighborhood of $x$, then $f$ is $C^n$ at $x$.
contDiffWithinAt_iff_contDiffAt theorem
(h : s ∈ 𝓝 x) : ContDiffWithinAt π•œ n f s x ↔ ContDiffAt π•œ n f x
Full source 
theorem contDiffWithinAt_iff_contDiffAt (h : s ∈ 𝓝 x) :
    ContDiffWithinAtContDiffWithinAt π•œ n f s x ↔ ContDiffAt π•œ n f x := by
  rw [← univ_inter s, contDiffWithinAt_inter h, contDiffWithinAt_univ]
Equivalence of $C^n$ Differentiability Within a Neighborhood and at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For a set $s \subseteq E$ and a point $x \in E$, if $s$ is a neighborhood of $x$, then $f$ is $C^n$ within $s$ at $x$ if and only if $f$ is $C^n$ at $x$.
IsOpen.contDiffOn_iff theorem
(hs : IsOpen s) : ContDiffOn π•œ n f s ↔ βˆ€ ⦃a⦄, a ∈ s β†’ ContDiffAt π•œ n f a
Full source 
theorem IsOpen.contDiffOn_iff (hs : IsOpen s) :
    ContDiffOnContDiffOn π•œ n f s ↔ βˆ€ ⦃a⦄, a ∈ s β†’ ContDiffAt π•œ n f a :=
  forallβ‚‚_congr fun _ => contDiffWithinAt_iff_contDiffAtcontDiffWithinAt_iff_contDiffAt ∘ hs.mem_nhds
Characterization of $C^n$ Differentiability on Open Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For an open set $s \subseteq E$, the function $f$ is $C^n$ on $s$ if and only if for every point $a \in s$, the function $f$ is $C^n$ at $a$.
ContDiffOn.contDiffAt theorem
(h : ContDiffOn π•œ n f s) (hx : s ∈ 𝓝 x) : ContDiffAt π•œ n f x
Full source 
theorem ContDiffOn.contDiffAt (h : ContDiffOn π•œ n f s) (hx : s ∈ 𝓝 x) :
    ContDiffAt π•œ n f x :=
  (h _ (mem_of_mem_nhds hx)).contDiffAt hx
$C^n$ differentiability on a neighborhood implies $C^n$ differentiability at a point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ on a set $s \subseteq E$ and $s$ is a neighborhood of a point $x \in E$, then $f$ is $C^n$ at $x$.
ContDiffAt.congr_of_eventuallyEq theorem
(h : ContDiffAt π•œ n f x) (hg : f₁ =αΆ [𝓝 x] f) : ContDiffAt π•œ n f₁ x
Full source 
theorem ContDiffAt.congr_of_eventuallyEq (h : ContDiffAt π•œ n f x) (hg : f₁ =αΆ [𝓝 x] f) :
    ContDiffAt π•œ n f₁ x :=
  h.congr_of_eventuallyEq_of_mem (by rwa [nhdsWithin_univ]) (mem_univ x)
Preservation of $C^n$ Differentiability under Eventual Equality at a Point
Informal description
Let $f, f_1 : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$. If $f$ is $C^n$ at a point $x \in E$ and $f_1$ is eventually equal to $f$ in a neighborhood of $x$, then $f_1$ is also $C^n$ at $x$.
ContDiffAt.of_le theorem
(h : ContDiffAt π•œ n f x) (hmn : m ≀ n) : ContDiffAt π•œ m f x
Full source 
theorem ContDiffAt.of_le (h : ContDiffAt π•œ n f x) (hmn : m ≀ n) : ContDiffAt π•œ m f x :=
  ContDiffWithinAt.of_le h hmn
Decreasing Differentiability Order for $C^n$ Functions at a Point
Informal description
Let $f : E \to F$ be a function between normed vector spaces over a nontrivially normed field $\mathbb{K}$. If $f$ is $C^n$ at a point $x \in E$ and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then $f$ is $C^m$ at $x$.
ContDiffAt.continuousAt theorem
(h : ContDiffAt π•œ n f x) : ContinuousAt f x
Full source 
theorem ContDiffAt.continuousAt (h : ContDiffAt π•œ n f x) : ContinuousAt f x := by
  simpa [continuousWithinAt_univ] using h.continuousWithinAt
$C^n$ differentiability implies continuity at a point
Informal description
If a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^n$ at a point $x \in E$, then $f$ is continuous at $x$.
ContDiffAt.analyticAt theorem
(h : ContDiffAt π•œ Ο‰ f x) : AnalyticAt π•œ f x
Full source 
theorem ContDiffAt.analyticAt (h : ContDiffAt π•œ Ο‰ f x) : AnalyticAt π•œ f x := by
  rw [← contDiffWithinAt_univ] at h
  rw [← analyticWithinAt_univ]
  exact h.analyticWithinAt
Analyticity of $C^\omega$ Functions at a Point
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^\omega$ (analytic) at a point $x \in E$, then $f$ is analytic at $x$.
AnalyticAt.contDiffAt theorem
[CompleteSpace F] (h : AnalyticAt π•œ f x) : ContDiffAt π•œ n f x
Full source 
/-- In a complete space, a function which is analytic at a point is also `C^Ο‰` there.
Note that the same statement for `AnalyticOn` does not require completeness, see
`AnalyticOn.contDiffOn`. -/
theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt π•œ f x) :
    ContDiffAt π•œ n f x := by
  rw [← contDiffWithinAt_univ]
  rw [← analyticWithinAt_univ] at h
  exact h.contDiffWithinAt
Analyticity implies $C^n$ differentiability at a point in complete spaces
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, with $F$ complete. If a function $f \colon E \to F$ is analytic at a point $x \in E$, then $f$ is $C^n$ at $x$ for any extended natural number $n \in \mathbb{N}_\infty$.
contDiffWithinAt_compl_self theorem
: ContDiffWithinAt π•œ n f { x }ᢜ x ↔ ContDiffAt π•œ n f x
Full source 
@[simp]
theorem contDiffWithinAt_compl_self :
    ContDiffWithinAtContDiffWithinAt π•œ n f {x}ᢜ x ↔ ContDiffAt π•œ n f x := by
  rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_univ]
Equivalence of \( C^n \) Differentiability at a Point and within its Complement
Informal description
For a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and for any extended natural number \( n \), the following are equivalent: 1. \( f \) is \( C^n \) within the complement of the singleton set \(\{x\}\) at \( x \). 2. \( f \) is \( C^n \) at the point \( x \).
ContDiffAt.differentiableAt theorem
(h : ContDiffAt π•œ n f x) (hn : 1 ≀ n) : DifferentiableAt π•œ f x
Full source 
/-- If a function is `C^n` with `n β‰₯ 1` at a point, then it is differentiable there. -/
theorem ContDiffAt.differentiableAt (h : ContDiffAt π•œ n f x) (hn : 1 ≀ n) :
    DifferentiableAt π•œ f x := by
  simpa [hn, differentiableWithinAt_univ] using h.differentiableWithinAt
Differentiability of $C^n$ functions at a point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ at a point $x \in E$ for some $n \geq 1$, then $f$ is differentiable at $x$.
ContDiffAt.contDiffOn theorem
(h : ContDiffAt π•œ n f x) (hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰) : βˆƒ u ∈ 𝓝 x, ContDiffOn π•œ m f u
Full source 
nonrec lemma ContDiffAt.contDiffOn (h : ContDiffAt π•œ n f x) (hm : m ≀ n) (h' : m = ∞ β†’ n = Ο‰):
    βˆƒ u ∈ 𝓝 x, ContDiffOn π•œ m f u := by
  simpa [nhdsWithin_univ] using h.contDiffOn hm h'
Local $C^m$ Differentiability from $C^n$ Differentiability at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ at a point $x \in E$. For any extended natural number $m \leq n$ (with the condition that if $m = \infty$ then $n = \omega$), there exists a neighborhood $u$ of $x$ such that $f$ is $C^m$ on $u$.
contDiffAt_succ_iff_hasFDerivAt theorem
{n : β„•} : ContDiffAt π•œ (n + 1) f x ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F, (βˆƒ u ∈ 𝓝 x, βˆ€ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt π•œ n f' x
Full source 
/-- A function is `C^(n + 1)` at a point iff locally, it has a derivative which is `C^n`. -/
theorem contDiffAt_succ_iff_hasFDerivAt {n : β„•} :
    ContDiffAtContDiffAt π•œ (n + 1) f x ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F,
      (βˆƒ u ∈ 𝓝 x, βˆ€ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt π•œ n f' x := by
  rw [← contDiffWithinAt_univ, contDiffWithinAt_succ_iff_hasFDerivWithinAt (by simp)]
  simp only [nhdsWithin_univ, exists_prop, mem_univ, insert_eq_of_mem]
  constructor
  · rintro ⟨u, H, -, f', h_fderiv, h_cont_diff⟩
    rcases mem_nhds_iff.mp H with ⟨t, htu, ht, hxt⟩
    refine ⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt H⟩
    refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩
    intro y hyt
    refine (h_fderiv y (htu hyt)).hasFDerivAt ?_
    exact mem_nhds_iff.mpr ⟨t, htu, ht, hyt⟩
  · rintro ⟨f', ⟨u, H, h_fderiv⟩, h_cont_diff⟩
    refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.contDiffWithinAt⟩
    exact (h_fderiv x hxu).hasFDerivWithinAt
Characterization of $C^{n+1}$ Differentiability via Local Existence of $C^n$ Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any natural number $n$, the following are equivalent: 1. $f$ is $C^{n+1}$ at a point $x \in E$. 2. There exists a FrΓ©chet derivative function $f' : E \to (E \toL[\mathbb{K}] F)$ and a neighborhood $u$ of $x$ such that: - For all $y \in u$, $f$ has FrΓ©chet derivative $f'(y)$ at $y$. - $f'$ is $C^n$ at $x$.
ContDiffAt.eventually theorem
(h : ContDiffAt π•œ n f x) (h' : n β‰  ∞) : βˆ€αΆ  y in 𝓝 x, ContDiffAt π•œ n f y
Full source 
protected theorem ContDiffAt.eventually (h : ContDiffAt π•œ n f x) (h' : n β‰  ∞) :
    βˆ€αΆ  y in 𝓝 x, ContDiffAt π•œ n f y := by
  simpa [nhdsWithin_univ] using ContDiffWithinAt.eventually h h'
Local persistence of $C^n$ differentiability at a point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ at a point $x \in E$ for some finite $n \in \mathbb{N}_\infty$. Then there exists a neighborhood of $x$ such that $f$ is $C^n$ at every point $y$ in this neighborhood.
iteratedFDerivWithin_eq_iteratedFDeriv theorem
{n : β„•} (hs : UniqueDiffOn π•œ s) (h : ContDiffAt π•œ n f x) (hx : x ∈ s) : iteratedFDerivWithin π•œ n f s x = iteratedFDeriv π•œ n f x
Full source 
theorem iteratedFDerivWithin_eq_iteratedFDeriv {n : β„•}
    (hs : UniqueDiffOn π•œ s) (h : ContDiffAt π•œ n f x) (hx : x ∈ s) :
    iteratedFDerivWithin π•œ n f s x = iteratedFDeriv π•œ n f x := by
  rw [← iteratedFDerivWithin_univ]
  rcases h.contDiffOn' le_rfl (by simp) with ⟨u, u_open, xu, hu⟩
  rw [← iteratedFDerivWithin_inter_open u_open xu,
    ← iteratedFDerivWithin_inter_open u_open xu (s := univ)]
  apply iteratedFDerivWithin_subset
  Β· exact inter_subset_inter_left _ (subset_univ _)
  Β· exact hs.inter u_open
  Β· apply uniqueDiffOn_univ.inter u_open
  Β· simpa using hu
  · exact ⟨hx, xu⟩
Agreement of Iterated Derivatives on Uniquely Differentiable Sets
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset with the unique differentiability property. For a function $f : E \to F$ that is $C^n$ at a point $x \in s$, the $n$-th iterated derivative of $f$ within $s$ at $x$ coincides with the $n$-th iterated derivative of $f$ in the whole space at $x$.
ContDiff definition
(n : WithTop β„•βˆž) (f : E β†’ F) : Prop
Full source 
/-- A function is continuously differentiable up to `n` if it admits derivatives up to
order `n`, which are continuous. Contrary to the case of definitions in domains (where derivatives
might not be unique) we do not need to localize the definition in space or time.
-/
def ContDiff (n : WithTop β„•βˆž) (f : E β†’ F) : Prop :=
  match n with
  | Ο‰ => βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpTo ⊀ f p
      ∧ βˆ€ i, AnalyticOnNhd π•œ (fun x ↦ p x i) univ
  | (n : β„•βˆž) => βˆƒ p : E β†’ FormalMultilinearSeries π•œ E F, HasFTaylorSeriesUpTo n f p
Continuously differentiable function of order \( n \) (\( C^n \))
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is said to be *continuously differentiable of order \( n \)* (denoted \( C^n \)) if it admits a formal Taylor series expansion up to order \( n \), where \( n \) is an element of the extended natural numbers \( \mathbb{N}_\infty \). - When \( n = \omega \) (i.e., \( \infty \)), this means there exists a formal multilinear series \( p : E \to \text{FormalMultilinearSeries} \mathbb{K} E F \) such that \( f \) has a Taylor series expansion up to infinite order, and each coefficient \( p_i \) of the series is analytic on a neighborhood of every point in \( E \). - When \( n \) is a finite extended natural number, it means there exists a formal multilinear series \( p \) such that \( f \) has a Taylor series expansion up to order \( n \).
HasFTaylorSeriesUpTo.contDiff theorem
{n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F} (hf : HasFTaylorSeriesUpTo n f f') : ContDiff π•œ n f
Full source 
/-- If `f` has a Taylor series up to `n`, then it is `C^n`. -/
theorem HasFTaylorSeriesUpTo.contDiff {n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F}
    (hf : HasFTaylorSeriesUpTo n f f') : ContDiff π•œ n f :=
  ⟨f', hf⟩
Existence of Taylor Series Implies \( C^n \) Differentiability
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( n \) be an extended natural number (i.e., \( n \in \mathbb{N}_\infty \)). If a function \( f : E \to F \) has a formal Taylor series \( f' \) up to order \( n \) (i.e., \( f' \) is a sequence of continuous multilinear maps satisfying the Taylor series conditions for \( f \) up to order \( n \)), then \( f \) is continuously differentiable of order \( n \) (denoted \( C^n \)).
contDiffOn_univ theorem
: ContDiffOn π•œ n f univ ↔ ContDiff π•œ n f
Full source 
theorem contDiffOn_univ : ContDiffOnContDiffOn π•œ n f univ ↔ ContDiff π•œ n f := by
  match n with
  | Ο‰ =>
    constructor
    Β· intro H
      use ftaylorSeriesWithin π•œ f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩
      rw [← analyticOn_univ]
      exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _
    · rintro ⟨p, hp, h'p⟩ x _
      exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
        fun i ↦ (h'p i).analyticOn⟩
  | (n : β„•βˆž) =>
    constructor
    Β· intro H
      use ftaylorSeriesWithin π•œ f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      exact H.ftaylorSeriesWithin uniqueDiffOn_univ
    · rintro ⟨p, hp⟩ x _ m hm
      exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩
Equivalence of Global \( C^n \) Differentiability and \( C^n \) Differentiability on the Entire Space
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^n \) on the entire space \( E \) if and only if it is \( C^n \) (i.e., continuously differentiable of order \( n \)) in the usual global sense.
contDiff_iff_contDiffAt theorem
: ContDiff π•œ n f ↔ βˆ€ x, ContDiffAt π•œ n f x
Full source 
theorem contDiff_iff_contDiffAt : ContDiffContDiff π•œ n f ↔ βˆ€ x, ContDiffAt π•œ n f x := by
  simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]
Global \( C^n \) Differentiability is Equivalent to Pointwise \( C^n \) Differentiability
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^n \) (continuously differentiable of order \( n \)) if and only if it is \( C^n \) at every point \( x \in E \).
ContDiff.contDiffAt theorem
(h : ContDiff π•œ n f) : ContDiffAt π•œ n f x
Full source 
theorem ContDiff.contDiffAt (h : ContDiff π•œ n f) : ContDiffAt π•œ n f x :=
  contDiff_iff_contDiffAt.1 h x
Global \( C^n \) Differentiability Implies Pointwise \( C^n \) Differentiability
Informal description
If a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^n \) (continuously differentiable of order \( n \)), then it is \( C^n \) at every point \( x \in E \).
ContDiff.contDiffWithinAt theorem
(h : ContDiff π•œ n f) : ContDiffWithinAt π•œ n f s x
Full source 
theorem ContDiff.contDiffWithinAt (h : ContDiff π•œ n f) : ContDiffWithinAt π•œ n f s x :=
  h.contDiffAt.contDiffWithinAt
Global $C^n$ Differentiability Implies Local $C^n$ Differentiability Within Any Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (continuously differentiable of order $n$) on $E$, then for any subset $s \subseteq E$ and any point $x \in E$, $f$ is $C^n$ within $s$ at $x$.
contDiff_infty theorem
: ContDiff π•œ ∞ f ↔ βˆ€ n : β„•, ContDiff π•œ n f
Full source 
theorem contDiff_infty : ContDiffContDiff π•œ ∞ f ↔ βˆ€ n : β„•, ContDiff π•œ n f := by
  simp [contDiffOn_univ.symm, contDiffOn_infty]
Characterization of Infinite Differentiability via Finite Differentiability
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is infinitely differentiable (i.e., $C^\infty$) if and only if it is $C^n$ for every natural number $n \in \mathbb{N}$.
contDiff_all_iff_nat theorem
: (βˆ€ n : β„•βˆž, ContDiff π•œ n f) ↔ βˆ€ n : β„•, ContDiff π•œ n f
Full source 
theorem contDiff_all_iff_nat : (βˆ€ n : β„•βˆž, ContDiff π•œ n f) ↔ βˆ€ n : β„•, ContDiff π•œ n f := by
  simp only [← contDiffOn_univ, contDiffOn_all_iff_nat]
Equivalence of Infinite Differentiability Conditions: Extended vs. Natural Numbers
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^n$ for all extended natural numbers $n \in \mathbb{N}_\infty$ if and only if it is $C^n$ for all natural numbers $n \in \mathbb{N}$.
ContDiff.contDiffOn theorem
(h : ContDiff π•œ n f) : ContDiffOn π•œ n f s
Full source 
theorem ContDiff.contDiffOn (h : ContDiff π•œ n f) : ContDiffOn π•œ n f s :=
  (contDiffOn_univ.2 h).mono (subset_univ _)
Global \( C^n \) Differentiability Implies Local \( C^n \) Differentiability on Subsets
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^n \) on the entire space \( E \), then for any subset \( s \subseteq E \), the function \( f \) is also \( C^n \) on \( s \).
contDiff_zero theorem
: ContDiff π•œ 0 f ↔ Continuous f
Full source 
@[simp]
theorem contDiff_zero : ContDiffContDiff π•œ 0 f ↔ Continuous f := by
  rw [← contDiffOn_univ, continuous_iff_continuousOn_univ]
  exact contDiffOn_zero
Equivalence of \( C^0 \) Differentiability and Continuity
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^0 \) (i.e., continuously differentiable of order 0) if and only if it is continuous.
contDiffAt_zero theorem
: ContDiffAt π•œ 0 f x ↔ βˆƒ u ∈ 𝓝 x, ContinuousOn f u
Full source 
theorem contDiffAt_zero : ContDiffAtContDiffAt π•œ 0 f x ↔ βˆƒ u ∈ 𝓝 x, ContinuousOn f u := by
  rw [← contDiffWithinAt_univ]; simp [contDiffWithinAt_zero, nhdsWithin_univ]
Characterization of \( C^0 \) Differentiability at a Point via Local Continuity
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^0 \) at a point \( x \in E \) if and only if there exists a neighborhood \( u \) of \( x \) such that \( f \) is continuous on \( u \).
contDiffAt_one_iff theorem
: ContDiffAt π•œ 1 f x ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F, βˆƒ u ∈ 𝓝 x, ContinuousOn f' u ∧ βˆ€ x ∈ u, HasFDerivAt f (f' x) x
Full source 
theorem contDiffAt_one_iff :
    ContDiffAtContDiffAt π•œ 1 f x ↔
      βˆƒ f' : E β†’ E β†’L[π•œ] F, βˆƒ u ∈ 𝓝 x, ContinuousOn f' u ∧ βˆ€ x ∈ u, HasFDerivAt f (f' x) x := by
  rw [show (1 : WithTop β„•βˆž) = (0 : β„•) + 1 from rfl]
  simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : β„•) : WithTop β„•βˆž) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]
Characterization of $C^1$ Differentiability at a Point via Continuous Derivative
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^1$ at a point $x \in E$ if and only if there exists a continuous linear map $f' : E \to E \toL[\mathbb{K}] F$ and a neighborhood $u$ of $x$ such that $f'$ is continuous on $u$ and $f$ has FrΓ©chet derivative $f'(x)$ at every point $x \in u$.
ContDiff.of_le theorem
(h : ContDiff π•œ n f) (hmn : m ≀ n) : ContDiff π•œ m f
Full source 
theorem ContDiff.of_le (h : ContDiff π•œ n f) (hmn : m ≀ n) : ContDiff π•œ m f :=
  contDiffOn_univ.1 <| (contDiffOn_univ.2 h).of_le hmn
Decreasing Differentiability Order for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (i.e., $n$-times continuously differentiable) and $m \leq n$ in the extended natural numbers $\mathbb{N}_\infty$, then $f$ is $C^m$.
ContDiff.of_succ theorem
(h : ContDiff π•œ (n + 1) f) : ContDiff π•œ n f
Full source 
theorem ContDiff.of_succ (h : ContDiff π•œ (n + 1) f) : ContDiff π•œ n f :=
  h.of_le le_self_add
Decreasing differentiability order: $C^{n+1}$ implies $C^n$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^{n+1}$ (i.e., $(n+1)$-times continuously differentiable), then $f$ is $C^n$.
ContDiff.one_of_succ theorem
(h : ContDiff π•œ (n + 1) f) : ContDiff π•œ 1 f
Full source 
theorem ContDiff.one_of_succ (h : ContDiff π•œ (n + 1) f) : ContDiff π•œ 1 f := by
  apply h.of_le le_add_self
$C^{n+1}$ functions are $C^1$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$. If a function $f : E \to F$ is $(n+1)$-times continuously differentiable (i.e., $C^{n+1}$), then it is continuously differentiable of order 1 (i.e., $C^1$).
ContDiff.continuous theorem
(h : ContDiff π•œ n f) : Continuous f
Full source 
theorem ContDiff.continuous (h : ContDiff π•œ n f) : Continuous f :=
  contDiff_zero.1 (h.of_le bot_le)
Continuity of $C^n$ Functions
Informal description
If a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^n$ (continuously differentiable of order $n$), then $f$ is continuous.
ContDiff.differentiable theorem
(h : ContDiff π•œ n f) (hn : 1 ≀ n) : Differentiable π•œ f
Full source 
/-- If a function is `C^n` with `n β‰₯ 1`, then it is differentiable. -/
theorem ContDiff.differentiable (h : ContDiff π•œ n f) (hn : 1 ≀ n) : Differentiable π•œ f :=
  differentiableOn_univ.1 <| (contDiffOn_univ.2 h).differentiableOn hn
Differentiability of $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$. If a function $f : E \to F$ is $C^n$ for some $n \geq 1$, then $f$ is differentiable on $E$.
contDiff_iff_forall_nat_le theorem
{n : β„•βˆž} : ContDiff π•œ n f ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiff π•œ m f
Full source 
theorem contDiff_iff_forall_nat_le {n : β„•βˆž} :
    ContDiffContDiff π•œ n f ↔ βˆ€ m : β„•, ↑m ≀ n β†’ ContDiff π•œ m f := by
  simp_rw [← contDiffOn_univ]; exact contDiffOn_iff_forall_nat_le
Characterization of $C^n$ Differentiability via Finite Orders
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any extended natural number $n \in \mathbb{N}_\infty$, the function $f$ is $C^n$ (continuously differentiable of order $n$) if and only if for every natural number $m \in \mathbb{N}$ such that $m \leq n$, the function $f$ is $C^m$.
contDiff_succ_iff_hasFDerivAt theorem
{n : β„•} : ContDiff π•œ (n + 1) f ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F, ContDiff π•œ n f' ∧ βˆ€ x, HasFDerivAt f (f' x) x
Full source 
/-- A function is `C^(n+1)` iff it has a `C^n` derivative. -/
theorem contDiff_succ_iff_hasFDerivAt {n : β„•} :
    ContDiffContDiff π•œ (n + 1) f ↔
      βˆƒ f' : E β†’ E β†’L[π•œ] F, ContDiff π•œ n f' ∧ βˆ€ x, HasFDerivAt f (f' x) x := by
  simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ, Set.mem_univ, forall_true_left,
    contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ,
    WithTop.natCast_ne_top, analyticOn_univ, false_implies, true_and]
Characterization of $C^{n+1}$ Differentiability via Existence of $C^n$ Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any natural number $n \in \mathbb{N}$, the following are equivalent: 1. The function $f$ is $C^{n+1}$ (continuously differentiable of order $n+1$). 2. There exists a function $f' : E \to E \toL[\mathbb{K}] F$ such that: - $f'$ is $C^n$. - For every $x \in E$, $f$ has FrΓ©chet derivative $f'(x)$ at $x$.
contDiff_one_iff_hasFDerivAt theorem
: ContDiff π•œ 1 f ↔ βˆƒ f' : E β†’ E β†’L[π•œ] F, Continuous f' ∧ βˆ€ x, HasFDerivAt f (f' x) x
Full source 
theorem contDiff_one_iff_hasFDerivAt : ContDiffContDiff π•œ 1 f ↔
    βˆƒ f' : E β†’ E β†’L[π•œ] F, Continuous f' ∧ βˆ€ x, HasFDerivAt f (f' x) x := by
  convert contDiff_succ_iff_hasFDerivAt using 4; simp
Characterization of $C^1$ Differentiability via Continuous FrΓ©chet Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. The following are equivalent: 1. $f$ is continuously differentiable of order 1 ($C^1$). 2. There exists a continuous function $f' : E \to E \toL[\mathbb{K}] F$ such that for every $x \in E$, $f$ has FrΓ©chet derivative $f'(x)$ at $x$.
AnalyticOn.contDiff theorem
(hf : AnalyticOn π•œ f univ) : ContDiff π•œ n f
Full source 
theorem AnalyticOn.contDiff (hf : AnalyticOn π•œ f univ) : ContDiff π•œ n f := by
  rw [← contDiffOn_univ]
  exact hf.contDiffOn (n := n) uniqueDiffOn_univ
Analyticity Implies Infinite Differentiability on the Entire Space
Informal description
If a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is analytic on the entire space \( E \), then it is continuously differentiable of order \( n \) (i.e., \( C^n \)) for any extended natural number \( n \).
AnalyticOnNhd.contDiff theorem
(hf : AnalyticOnNhd π•œ f univ) : ContDiff π•œ n f
Full source 
theorem AnalyticOnNhd.contDiff (hf : AnalyticOnNhd π•œ f univ) : ContDiff π•œ n f :=
  hf.analyticOn.contDiff
Analyticity on Neighborhood of Entire Space Implies Continuous Differentiability of Order \( n \)
Informal description
If a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is analytic on a neighborhood of the entire space \( E \), then \( f \) is continuously differentiable of order \( n \) (i.e., \( C^n \)) for any extended natural number \( n \).
ContDiff.analyticOnNhd theorem
(h : ContDiff π•œ Ο‰ f) : AnalyticOnNhd π•œ f s
Full source 
theorem ContDiff.analyticOnNhd (h : ContDiff π•œ Ο‰ f) : AnalyticOnNhd π•œ f s := by
  rw [← contDiffOn_univ] at h
  have := h.analyticOn
  rw [analyticOn_univ] at this
  exact this.mono (subset_univ _)
Analyticity of \( C^\omega \) Functions on Neighborhoods of Subsets
Informal description
Let \( E \) and \( F \) be normed vector spaces over a nontrivially normed field \( \mathbb{K} \), and let \( f : E \to F \) be a function. If \( f \) is \( C^\omega \) (i.e., analytic) on the entire space \( E \), then \( f \) is analytic on a neighborhood of any subset \( s \subseteq E \).
contDiff_omega_iff_analyticOnNhd theorem
: ContDiff π•œ Ο‰ f ↔ AnalyticOnNhd π•œ f univ
Full source 
theorem contDiff_omega_iff_analyticOnNhd :
    ContDiffContDiff π•œ Ο‰ f ↔ AnalyticOnNhd π•œ f univ :=
  ⟨fun h ↦ h.analyticOnNhd, fun h ↦ h.contDiff⟩
Characterization of Analytic Functions via Neighborhood Analyticity
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^\omega$ (i.e., analytic) if and only if it is analytic on a neighborhood of the entire space $E$.
ContDiff.ftaylorSeries theorem
(hf : ContDiff π•œ n f) : HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f)
Full source 
/-- When a function is `C^n`, it admits `ftaylorSeries π•œ f` as a Taylor series up
to order `n` in `s`. -/
theorem ContDiff.ftaylorSeries (hf : ContDiff π•œ n f) :
    HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f) := by
  simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    at hf ⊒
  exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ
Existence of Taylor Series for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that is $C^n$ (i.e., $n$-times continuously differentiable). Then $f$ admits the formal Taylor series $\text{ftaylorSeries}\, \mathbb{K}\, f$ as a valid Taylor series expansion up to order $n$ on $E$.
contDiff_iff_ftaylorSeries theorem
{n : β„•βˆž} : ContDiff π•œ n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f)
Full source 
/-- For `n : β„•βˆž`, a function is `C^n` iff it admits `ftaylorSeries π•œ f`
as a Taylor series up to order `n`. -/
theorem contDiff_iff_ftaylorSeries {n : β„•βˆž} :
    ContDiffContDiff π•œ n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f) := by
  constructor
  Β· rw [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
    exact fun h ↦ ContDiffOn.ftaylorSeriesWithin h uniqueDiffOn_univ
  Β· exact fun h ↦ ⟨ftaylorSeries π•œ f, h⟩
Characterization of \( C^n \) Functions via Taylor Series
Informal description
For any extended natural number \( n \in \mathbb{N}_\infty \), a function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^n \) if and only if it admits the formal Taylor series \( \text{ftaylorSeries}\, \mathbb{K}\, f \) as a valid Taylor series expansion up to order \( n \).
contDiff_iff_continuous_differentiable theorem
{n : β„•βˆž} : ContDiff π•œ n f ↔ (βˆ€ m : β„•, m ≀ n β†’ Continuous fun x => iteratedFDeriv π•œ m f x) ∧ βˆ€ m : β„•, m < n β†’ Differentiable π•œ fun x => iteratedFDeriv π•œ m f x
Full source 
theorem contDiff_iff_continuous_differentiable {n : β„•βˆž} :
    ContDiffContDiff π•œ n f ↔
      (βˆ€ m : β„•, m ≀ n β†’ Continuous fun x => iteratedFDeriv π•œ m f x) ∧
        βˆ€ m : β„•, m < n β†’ Differentiable π•œ fun x => iteratedFDeriv π•œ m f x := by
  simp [contDiffOn_univ.symm, continuous_iff_continuousOn_univ, differentiableOn_univ.symm,
    iteratedFDerivWithin_univ, contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ]
Characterization of $C^n$ Differentiability via Continuity and Differentiability of Iterated Derivatives
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any extended natural number $n \in \mathbb{N}_\infty$, the function $f$ is $C^n$ (i.e., $n$-times continuously differentiable) if and only if: 1. For every natural number $m \leq n$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDeriv}_{\mathbb{K}}^m f$ is continuous on $E$. 2. For every natural number $m < n$, the $m$-th iterated FrΓ©chet derivative is differentiable on $E$.
contDiff_nat_iff_continuous_differentiable theorem
{n : β„•} : ContDiff π•œ n f ↔ (βˆ€ m : β„•, m ≀ n β†’ Continuous fun x => iteratedFDeriv π•œ m f x) ∧ βˆ€ m : β„•, m < n β†’ Differentiable π•œ fun x => iteratedFDeriv π•œ m f x
Full source 
theorem contDiff_nat_iff_continuous_differentiable {n : β„•} :
    ContDiffContDiff π•œ n f ↔
      (βˆ€ m : β„•, m ≀ n β†’ Continuous fun x => iteratedFDeriv π•œ m f x) ∧
        βˆ€ m : β„•, m < n β†’ Differentiable π•œ fun x => iteratedFDeriv π•œ m f x := by
  rw [← WithTop.coe_natCast, contDiff_iff_continuous_differentiable]
  simp
Characterization of $C^n$ Differentiability via Continuity and Differentiability of Iterated Derivatives for Finite $n$
Informal description
For a natural number $n$, a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is $C^n$ (i.e., $n$-times continuously differentiable) if and only if: 1. For every natural number $m \leq n$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDeriv}_{\mathbb{K}}^m f$ is continuous on $E$. 2. For every natural number $m < n$, the $m$-th iterated FrΓ©chet derivative is differentiable on $E$.
ContDiff.continuous_iteratedFDeriv theorem
{m : β„•} (hm : m ≀ n) (hf : ContDiff π•œ n f) : Continuous fun x => iteratedFDeriv π•œ m f x
Full source 
/-- If `f` is `C^n` then its `m`-times iterated derivative is continuous for `m ≀ n`. -/
theorem ContDiff.continuous_iteratedFDeriv {m : β„•} (hm : m ≀ n) (hf : ContDiff π•œ n f) :
    Continuous fun x => iteratedFDeriv π•œ m f x :=
  (contDiff_iff_continuous_differentiable.mp (hf.of_le hm)).1 m le_rfl
Continuity of Iterated Derivatives for $C^n$ Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a $C^n$ function. For any natural number $m \leq n$, the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDeriv}_{\mathbb{K}}^m f$ is continuous on $E$.
ContDiff.differentiable_iteratedFDeriv theorem
{m : β„•} (hm : m < n) (hf : ContDiff π•œ n f) : Differentiable π•œ fun x => iteratedFDeriv π•œ m f x
Full source 
/-- If `f` is `C^n` then its `m`-times iterated derivative is differentiable for `m < n`. -/
theorem ContDiff.differentiable_iteratedFDeriv {m : β„•} (hm : m < n) (hf : ContDiff π•œ n f) :
    Differentiable π•œ fun x => iteratedFDeriv π•œ m f x :=
  (contDiff_iff_continuous_differentiable.mp
    (hf.of_le (ENat.add_one_natCast_le_withTop_of_lt hm))).2 m (mod_cast lt_add_one m)
Differentiability of iterated derivatives for $C^n$ functions: $m < n \Rightarrow \text{iteratedFDeriv}^m f$ is differentiable
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a $C^n$ function (i.e., $n$-times continuously differentiable). Then for any natural number $m < n$, the $m$-th iterated FrΓ©chet derivative of $f$ is differentiable on $E$.
contDiff_of_differentiable_iteratedFDeriv theorem
{n : β„•βˆž} (h : βˆ€ m : β„•, m ≀ n β†’ Differentiable π•œ (iteratedFDeriv π•œ m f)) : ContDiff π•œ n f
Full source 
theorem contDiff_of_differentiable_iteratedFDeriv {n : β„•βˆž}
    (h : βˆ€ m : β„•, m ≀ n β†’ Differentiable π•œ (iteratedFDeriv π•œ m f)) : ContDiff π•œ n f :=
  contDiff_iff_continuous_differentiable.2
    ⟨fun m hm => (h m hm).continuous, fun m hm => h m (le_of_lt hm)⟩
Differentiability of Iterated Derivatives Implies $C^n$ Smoothness
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If for every natural number $m \leq n$ (where $n \in \mathbb{N}_\infty$), the $m$-th iterated FrΓ©chet derivative $\mathrm{iteratedFDeriv}_{\mathbb{K}}^m f$ is differentiable on $E$, then $f$ is $C^n$ (i.e., $n$-times continuously differentiable).
contDiff_succ_iff_fderiv theorem
: ContDiff π•œ (n + 1) f ↔ Differentiable π•œ f ∧ (n = Ο‰ β†’ AnalyticOnNhd π•œ f univ) ∧ ContDiff π•œ n (fderiv π•œ f)
Full source 
/-- A function is `C^(n + 1)` if and only if it is differentiable,
and its derivative (formulated in terms of `fderiv`) is `C^n`. -/
theorem contDiff_succ_iff_fderiv :
    ContDiffContDiff π•œ (n + 1) f ↔ Differentiable π•œ f ∧ (n = Ο‰ β†’ AnalyticOnNhd π•œ f univ) ∧
      ContDiff π•œ n (fderiv π•œ f) := by
  simp only [← contDiffOn_univ, ← differentiableOn_univ, ← fderivWithin_univ,
    contDiffOn_succ_iff_fderivWithin uniqueDiffOn_univ, analyticOn_univ]
Characterization of $C^{n+1}$ Differentiability via Differentiability and $C^n$ Differentiability of the Derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. For any extended natural number $n \in \mathbb{N}_\infty$, the following are equivalent: 1. The function $f$ is $C^{n+1}$ (i.e., continuously differentiable of order $n+1$). 2. The function $f$ is differentiable, and: - If $n = \omega$ (the analytic case), then $f$ is analytic on the entire space $E$. - The FrΓ©chet derivative of $f$, denoted by $fderiv_{\mathbb{K}} f$, is $C^n$.
contDiff_one_iff_fderiv theorem
: ContDiff π•œ 1 f ↔ Differentiable π•œ f ∧ Continuous (fderiv π•œ f)
Full source 
theorem contDiff_one_iff_fderiv :
    ContDiffContDiff π•œ 1 f ↔ Differentiable π•œ f ∧ Continuous (fderiv π•œ f) := by
  rw [← zero_add 1, contDiff_succ_iff_fderiv]
  simp
Characterization of $C^1$ functions via differentiability and continuous derivative
Informal description
A function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is continuously differentiable of order 1 (i.e., $C^1$) if and only if it is differentiable and its FrΓ©chet derivative $f'$ is continuous.
contDiff_infty_iff_fderiv theorem
: ContDiff π•œ ∞ f ↔ Differentiable π•œ f ∧ ContDiff π•œ ∞ (fderiv π•œ f)
Full source 
theorem contDiff_infty_iff_fderiv :
    ContDiffContDiff π•œ ∞ f ↔ Differentiable π•œ f ∧ ContDiff π•œ ∞ (fderiv π•œ f) := by
  rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]
  simp
Characterization of \( C^\infty \) Differentiability via Differentiability and \( C^\infty \) Differentiability of the Derivative
Informal description
A function \( f : E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \) is \( C^\infty \) (infinitely differentiable) if and only if it is differentiable and its FrΓ©chet derivative \( f' \) is also \( C^\infty \).
ContDiff.continuous_fderiv theorem
(h : ContDiff π•œ n f) (hn : 1 ≀ n) : Continuous (fderiv π•œ f)
Full source 
theorem ContDiff.continuous_fderiv (h : ContDiff π•œ n f) (hn : 1 ≀ n) :
    Continuous (fderiv π•œ f) :=
  (contDiff_one_iff_fderiv.1 (h.of_le hn)).2
Continuity of the FrΓ©chet Derivative for $C^n$ Functions ($n \geq 1$)
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (i.e., $n$-times continuously differentiable) for some $n \geq 1$, then its FrΓ©chet derivative $f'$ is continuous.
ContDiff.continuous_fderiv_apply theorem
(h : ContDiff π•œ n f) (hn : 1 ≀ n) : Continuous fun p : E Γ— E => (fderiv π•œ f p.1 : E β†’ F) p.2
Full source 
/-- If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
continuous. -/
theorem ContDiff.continuous_fderiv_apply (h : ContDiff π•œ n f) (hn : 1 ≀ n) :
    Continuous fun p : E Γ— E => (fderiv π•œ f p.1 : E β†’ F) p.2 :=
  have A : Continuous fun q : (E β†’L[π•œ] F) Γ— E => q.1 q.2 := isBoundedBilinearMap_apply.continuous
  have B : Continuous fun p : E Γ— E => (fderiv π•œ f p.1, p.2) :=
    ((h.continuous_fderiv hn).comp continuous_fst).prodMk continuous_snd
  A.comp B
Continuity of the Derivative Application for $C^n$ Functions ($n \geq 1$)
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ is $C^n$ (i.e., $n$-times continuously differentiable) for some $n \geq 1$, then the map $(x, v) \mapsto Df(x)(v)$ is continuous, where $Df(x)$ denotes the FrΓ©chet derivative of $f$ at $x$.