Higher differentiability in one dimension

The general theory of higher derivatives in Mathlib is developed using the Fréchet derivative fderiv; but for maps defined on the field, the one-dimensional derivative deriv is often easier to use. In this file, we reformulate some higher smoothness results in terms of deriv.

Tags

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series

theorem contDiffOn_succ_iff_derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s

A function is C^(n + 1) on a domain with unique derivatives if and only if it is differentiable there, and its derivative (formulated with derivWithin) is C^n.

theorem contDiffOn_infty_iff_derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (derivWithin f s) s

theorem contDiffOn_succ_iff_deriv_of_isOpen {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (deriv f) s

A function is C^(n + 1) on an open domain if and only if it is differentiable there, and its derivative (formulated with deriv) is C^n.

theorem contDiffOn_infty_iff_deriv_of_isOpen {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (deriv f) s

theorem ContDiffOn.derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (derivWithin f s) s

theorem ContDiffOn.deriv_of_isOpen {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (deriv f) s

theorem ContDiffOn.continuousOn_derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (h : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hn : 1 ≤ n) : ContinuousOn (derivWithin f s) s

theorem ContDiffOn.continuousOn_deriv_of_isOpen {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hn : 1 ≤ n) : ContinuousOn (deriv f) s

theorem ContDiffWithinAt.derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜} (H : ContDiffWithinAt 𝕜 n f s x) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 ≤ n) (hx : x ∈ s) : ContDiffWithinAt 𝕜 m (derivWithin f s) s x

theorem contDiff_succ_iff_deriv {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} : ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOn 𝕜 f Set.univ) ∧ ContDiff 𝕜 n (deriv f)

A function is C^(n + 1) if and only if it is differentiable, and its derivative (formulated in terms of deriv) is C^n.

theorem contDiff_one_iff_deriv {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (deriv f)

theorem contDiff_infty_iff_deriv {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} : ContDiff 𝕜 (↑⊤) f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 (↑⊤) (deriv f)

theorem ContDiff.continuous_deriv {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} (h : ContDiff 𝕜 n f) (hn : 1 ≤ n) : Continuous (deriv f)

theorem ContDiff.continuous_deriv_one {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (h : ContDiff 𝕜 1 f) : Continuous (deriv f)

theorem ContDiff.differentiable_deriv_two {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} (h : ContDiff 𝕜 2 f) : Differentiable 𝕜 (deriv f)

theorem ContDiffAt.derivWithin {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {x : 𝕜} (H : ContDiffAt 𝕜 n f x) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (deriv f) x

theorem ContDiff.deriv' {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} (h : ContDiff 𝕜 (n + 1) f) : ContDiff 𝕜 n (deriv f)

theorem ContDiff.iterate_deriv {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) {f : 𝕜 → F} : ContDiff 𝕜 (↑⊤) f → ContDiff 𝕜 (↑⊤) (deriv^[n] f)

theorem ContDiff.iterate_deriv' {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n k : ℕ) {f : 𝕜 → F} : ContDiff 𝕜 (↑(n + k)) f → ContDiff 𝕜 (↑n) (deriv^[k] f)