Documentation

Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

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) :
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) :
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) :

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) :
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) :
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) :
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) :
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) :
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 : โ„•) :

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.