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 Filter.EventuallyEq.iteratedDerivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f g : 𝕜 → F} (hfg : f =ᶠ[nhdsWithin x s] g) (hfg' : f x = g x) : iteratedDerivWithin n f s x = iteratedDerivWithin n g s x

theorem Filter.EventuallyEq.iteratedDerivWithin' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {f g : 𝕜 → F} {s t : Set 𝕜} (h : f =ᶠ[nhdsWithin x s] g) (ht : t ⊆ s) (n : ℕ) : iteratedDerivWithin n f t =ᶠ[nhdsWithin x s] iteratedDerivWithin n g t

theorem Filter.EventuallyEq.iteratedDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {f g : 𝕜 → F} {s : Set 𝕜} (h : f =ᶠ[nhdsWithin x s] g) (n : ℕ) : iteratedDerivWithin n f s =ᶠ[nhdsWithin x s] iteratedDerivWithin n g s

If two functions agree in a neighborhood within s, then so do their iterated derivatives.

theorem Filter.EventuallyEq.iteratedDerivWithin_eq_of_nhds_insert {𝕜 : Type u_7} {F : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hfg : f =ᶠ[nhdsWithin x (insert x s)] g) : iteratedDerivWithin n f s x = iteratedDerivWithin n g s x

theorem iteratedDerivWithin_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {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 : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f + g) s x = iteratedDerivWithin n f s x + iteratedDerivWithin n g s x

theorem iteratedDerivWithin_fun_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 : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (fun (z : 𝕜) => f z + g z) 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 𝕜} {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 𝕜} {f : 𝕜 → F} (hn : 0 < n) (c : F) : iteratedDerivWithin n (fun (z : 𝕜) => c - f z) s x = iteratedDerivWithin n (fun (z : 𝕜) => -f z) s x

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

theorem iteratedDerivWithin_fun_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : ContDiffWithinAt 𝕜 (↑n) f s x) : iteratedDerivWithin n (fun (w : 𝕜) => c • f w) s x = c • iteratedDerivWithin n f s x

@[simp]

theorem iteratedDerivWithin_const_smul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F) : iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x

A variant of iteratedDerivWithin_const_smul without differentiability assumption when the scalar multiplication is by division ring elements.

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

@[simp]

theorem iteratedDerivWithin_fun_const_smul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F) : iteratedDerivWithin n (fun (z : 𝕜) => c • f z) s x = c • iteratedDerivWithin n f s x

A variant of iteratedDerivWithin_fun_const_smul without differentiability assumption when the scalar multiplication is by division ring elements.

@[simp]

theorem iteratedDerivWithin_const_mul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (c : 𝕜') (f : 𝕜 → 𝕜') : iteratedDerivWithin n (fun (z : 𝕜) => c * f z) s x = c * iteratedDerivWithin n f s x

theorem iteratedDerivWithin_smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (v : F) : iteratedDerivWithin n (fun (y : 𝕜) => f y • v) s x = iteratedDerivWithin n f s x • v

@[simp]

theorem iteratedDerivWithin_mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (d : 𝔸) : iteratedDerivWithin n (fun (z : 𝕜) => f z * d) s x = iteratedDerivWithin n f s x * d

@[simp]

theorem iteratedDerivWithin_mul_const_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] (f : 𝕜 → 𝕜') (d : 𝕜') : iteratedDerivWithin n (fun (z : 𝕜) => f z * d) s x = iteratedDerivWithin n f s x * d

A variant of iteratedDerivWithin_mul_const without differentiability assumption when the scalar multiplication is by division ring elements.

@[simp]

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

theorem iteratedDerivWithin_fun_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (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 : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

theorem iteratedDerivWithin_comp_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {f : 𝕜 → F} (hf : ContDiffOn 𝕜 (↑n) f s) (c : 𝕜) (hs : Set.MapsTo (fun (x : 𝕜) => c * x) s s) : iteratedDerivWithin n (fun (x : 𝕜) => f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)

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

theorem iteratedDerivWithin_comp_const_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜) : iteratedDerivWithin n (fun (z : 𝕜) => f (c + z)) s = fun (x : 𝕜) => iteratedDerivWithin n f (c +ᵥ s) (c + x)

theorem iteratedDerivWithin_comp_add_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜) : iteratedDerivWithin n (fun (z : 𝕜) => f (z + c)) s = fun (x : 𝕜) => iteratedDerivWithin n f (c +ᵥ s) (x + c)

theorem iteratedDerivWithin_comp_sub_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜) : iteratedDerivWithin n (fun (z : 𝕜) => f (z - c)) s = fun (x : 𝕜) => iteratedDerivWithin n f (-c +ᵥ s) (x - c)

theorem iteratedDerivWithin_comp_const_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜) : iteratedDerivWithin n (fun (z : 𝕜) => f (c - z)) s = fun (x : 𝕜) => (-1) ^ n • iteratedDerivWithin n f (c +ᵥ -s) (c - x)

theorem iteratedDerivWithin_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) : iteratedDerivWithin n id s x = if n = 0 then x else if n = 1 then 1 else 0

theorem iteratedDerivWithin_fun_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) : iteratedDerivWithin n (fun (x : 𝕜) => x) s x = if n = 0 then x else if n = 1 then 1 else 0

Eta-expanded form of iteratedDerivWithin_id

theorem iteratedDerivWithin_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} {g : 𝕜 → F} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f • g) s x = ∑ i ∈ Finset.range (n + 1), n.choose i • iteratedDerivWithin i f s x • iteratedDerivWithin (n - i) g s x

theorem iteratedDerivWithin_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffWithinAt 𝕜 (↑n) f s x) (hg : ContDiffWithinAt 𝕜 (↑n) g s x) : iteratedDerivWithin n (f * g) s x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDerivWithin i f s x * iteratedDerivWithin (n - i) g s x

theorem iteratedDerivWithin_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) (h : UniqueDiffOn 𝕜 s) (m k : ℕ) : iteratedDerivWithin k (fun (x : 𝕜) => x ^ m) s x = ↑(m.descFactorial k) * x ^ (m - k)

theorem Filter.EventuallyEq.iteratedDeriv {𝕜 : Type u_7} [NontriviallyNormedField 𝕜] {F : Type u_8} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ f₂ : 𝕜 → F} {x : 𝕜} (h : f₁ =ᶠ[nhds x] f₂) (n : ℕ) : iteratedDeriv n f₁ =ᶠ[nhds x] iteratedDeriv n f₂

If two functions agree in a neighborhood, then so do their iterated derivatives.

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

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

Eta-expanded form of iteratedDeriv_add

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

@[simp]

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

@[simp]

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

Eta-expanded form of iteratedDeriv_neg

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

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

Eta-expanded form of iteratedDeriv_sub

theorem iteratedDeriv_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 (↑n) f x) (c : R) : iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

theorem iteratedDeriv_fun_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {R : Type u_3} [DistribSMul R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 (↑n) f x) (c : R) : iteratedDeriv n (fun (i : 𝕜) => c • f i) x = c • iteratedDeriv n f x

Eta-expanded form of iteratedDeriv_const_smul

@[simp]

theorem iteratedDeriv_const_smul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F) : iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

A variant of iteratedDeriv_const_smul without differentiability assumption when the scalar multiplication is by division ring elements.

@[simp]

theorem iteratedDeriv_fun_const_smul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕝 : Type u_4} [DivisionSemiring 𝕝] [Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] {n : ℕ} (c : 𝕝) (f : 𝕜 → F) : iteratedDeriv n (fun (x : 𝕜) => c • f x) x = c • iteratedDeriv n f x

A variant of iteratedDeriv_fun_const_smul without differentiability assumption when the scalar multiplication is by division ring elements.

theorem iteratedDeriv_smul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Module 𝔸 F] [IsBoundedSMul 𝔸 F] [IsScalarTower 𝕜 𝔸 F] {f : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (v : F) : iteratedDeriv n (fun (y : 𝕜) => f y • v) x = iteratedDeriv n f x • v

theorem iteratedDeriv_const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {n : ℕ} {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 (↑n) f x) : iteratedDeriv n (fun (x : 𝕜) => c * f x) x = c * iteratedDeriv n f x

@[simp]

theorem iteratedDeriv_const_mul_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (c : 𝕜') (f : 𝕜 → 𝕜') : iteratedDeriv n (fun (x : 𝕜) => c * f x) x = c * iteratedDeriv n f x

A variant of iteratedDeriv_const_mul without differentiability assumption when the multiplication is in a division ring.

@[simp]

theorem iteratedDeriv_mul_const_field {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜') : iteratedDeriv n (fun (x : 𝕜) => f x * c) x = iteratedDeriv n f x * c

A variant of iteratedDeriv_mul_const without differentiability assumption when the multiplication is in a division ring.

@[simp]

theorem iteratedDeriv_div_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_6} [NormedDivisionRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] {n : ℕ} (f : 𝕜 → 𝕜') (c : 𝕜') : iteratedDeriv n (fun (x : 𝕜) => f x / c) x = iteratedDeriv n f x / c

theorem iteratedDeriv_comp_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)

theorem iteratedDeriv_comp_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)

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 iteratedDeriv_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} : iteratedDeriv n id x = if n = 0 then x else if n = 1 then 1 else 0

theorem iteratedDeriv_fun_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} : iteratedDeriv n (fun (x : 𝕜) => x) x = if n = 0 then x else if n = 1 then 1 else 0

Eta-expanded form of iteratedDeriv_id

theorem iteratedDeriv_fun_id_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} : iteratedDeriv n (fun (a : 𝕜) => a) 0 = if n = 1 then 1 else 0

theorem iteratedDeriv_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (f * g) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x

theorem iteratedDeriv_fun_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸} (hf : ContDiffAt 𝕜 (↑n) f x) (hg : ContDiffAt 𝕜 (↑n) g x) : iteratedDeriv n (fun (i : 𝕜) => f i * g i) x = ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x

Eta-expanded form of iteratedDeriv_mul

@[simp]

theorem iteratedDeriv_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {x : 𝕜} (m k : ℕ) : iteratedDeriv k (fun (x : 𝕜) => x ^ m) x = ↑(m.descFactorial k) * x ^ (m - k)

theorem iteratedDeriv_fun_pow_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n m : ℕ} : iteratedDeriv n (fun (x : 𝕜) => x ^ m) 0 = ↑(if n = m then m.factorial else 0)

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 : EqOn f g s) (hs : IsOpen s) (n : ℕ) : EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Invariance of iterated derivatives under translation

theorem iteratedDeriv_comp_const_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [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} [NontriviallyNormedField 𝕜] {F : Type u_2} [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.

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

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

Iterated derivatives of sums

theorem iteratedDerivWithin_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜} (hx : x ∈ s) (hs : UniqueDiffOn 𝕜 s) (hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) : iteratedDerivWithin n (∑ i ∈ I, f i) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x

theorem iteratedDerivWithin_fun_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜} (hx : x ∈ s) (hs : UniqueDiffOn 𝕜 s) (hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) : iteratedDerivWithin n (fun (x : 𝕜) => ∑ i ∈ I, f i x) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x

theorem iteratedDeriv_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} (hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) : iteratedDeriv n (∑ i ∈ I, f i) x = ∑ i ∈ I, iteratedDeriv n (f i) x

theorem iteratedDeriv_fun_sum {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} (hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n) (f i) x) : iteratedDeriv n (fun (z : 𝕜) => ∑ i ∈ I, f i z) x = ∑ i ∈ I, iteratedDeriv n (f i) x