One-dimensional iterated derivatives

This file contains a number of further results on iteratedDerivWithin that need more imports than are available in Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean.

theorem iteratedDerivWithin_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} (h : UniqueDiffOn 𝕜 s) {f g : 𝕜 → F} (hfg : Set.EqOn f g s) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) s

theorem iteratedDerivWithin_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f g : 𝕜 → F} (hf : ContDiffOn 𝕜 (↑n) f s) (hg : ContDiffOn 𝕜 (↑n) g s) : iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

theorem iteratedDerivWithin_const_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDerivWithin n (fun (z : 𝕜) => c + f z) s x = iteratedDerivWithin n f s x

theorem iteratedDerivWithin_const_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDerivWithin n (fun (z : 𝕜) => c - f z) s x = iteratedDerivWithin n (fun (z : 𝕜) => -f z) s x

@[deprecated iteratedDerivWithin_const_sub]

theorem iteratedDerivWithin_const_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDerivWithin n (fun (z : 𝕜) => c - f z) s x = iteratedDerivWithin n (fun (z : 𝕜) => -f z) s x

Alias of iteratedDerivWithin_const_sub.

theorem iteratedDerivWithin_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} (c : R) (hf : ContDiffOn 𝕜 (↑n) f s) : iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

Note: this is unrelated to iteratedDeriv_const_smul, where the scalar multiplication works on the domain.

theorem iteratedDerivWithin_const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) (c : 𝕜) {f : 𝕜 → 𝕜} (hf : ContDiffOn 𝕜 (↑n) f s) : iteratedDerivWithin n (fun (z : 𝕜) => c * f z) s x = c * iteratedDerivWithin n f s x

Note: this is unrelated to iteratedDeriv_const_mul, where the multiplication works on the domain.

theorem iteratedDerivWithin_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) (f : 𝕜 → F) : iteratedDerivWithin n (-f) s x = -iteratedDerivWithin n f s x

theorem iteratedDerivWithin_neg' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) (f : 𝕜 → F) : iteratedDerivWithin n (fun (z : 𝕜) => -f z) s x = -iteratedDerivWithin n f s x

theorem iteratedDerivWithin_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f g : 𝕜 → F} (hf : ContDiffOn 𝕜 (↑n) f s) (hg : ContDiffOn 𝕜 (↑n) g s) : iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

theorem iteratedDeriv_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiff 𝕜 (↑n) f) (hg : ContDiff 𝕜 (↑n) g) : iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x

theorem iteratedDeriv_const_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDeriv n (fun (z : 𝕜) => c + f z) x = iteratedDeriv n f x

theorem iteratedDeriv_const_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDeriv n (fun (z : 𝕜) => c - f z) x = iteratedDeriv n (-f) x

theorem iteratedDeriv_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (fun (x : 𝕜) => -f x) a = -iteratedDeriv n f a

theorem iteratedDeriv_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {f g : 𝕜 → F} (hf : ContDiff 𝕜 (↑n) f) (hg : ContDiff 𝕜 (↑n) g) : iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x

theorem iteratedDeriv_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} (h : ContDiff 𝕜 (↑n) f) (c : 𝕜) : (iteratedDeriv n fun (x : 𝕜) => f (c * x)) = fun (x : 𝕜) => c ^ n • iteratedDeriv n f (c * x)

Note: this is unrelated to iteratedDerivWithin_const_smul, where the scalar multiplication works on the codomain.

theorem iteratedDeriv_const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiff 𝕜 (↑n) f) (c : 𝕜) : (iteratedDeriv n fun (x : 𝕜) => f (c * x)) = fun (x : 𝕜) => c ^ n * iteratedDeriv n f (c * x)

Note: this is unrelated to iteratedDerivWithin_const_mul, where the multiplication works on the codomain.

theorem iteratedDeriv_comp_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (a : 𝕜) : iteratedDeriv n (fun (x : 𝕜) => f (-x)) a = (-1) ^ n • iteratedDeriv n f (-a)

theorem Filter.EventuallyEq.iteratedDeriv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} (hfg : f =ᶠ[nhds x] g) : iteratedDeriv n f x = iteratedDeriv n g x

theorem Set.EqOn.iteratedDeriv_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {f g : 𝕜 → F} (hfg : Set.EqOn f g s) (hs : IsOpen s) (n : ℕ) : Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Invariance of iterated derivatives under translation

theorem iteratedDeriv_comp_const_add {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun (z : 𝕜) => f (s + z)) = fun (t : 𝕜) => iteratedDeriv n f (s + t)

The iterated derivative commutes with shifting the function by a constant on the left.

theorem iteratedDeriv_comp_add_const {𝕜 : Type u_1} {F : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (s : 𝕜) : (iteratedDeriv n fun (z : 𝕜) => f (z + s)) = fun (t : 𝕜) => iteratedDeriv n f (t + s)

The iterated derivative commutes with shifting the function by a constant on the right.