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 : 𝕜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 : 𝕜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_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
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) :
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
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 : 𝕜F} {g : 𝕜F} (hf : ContDiffOn 𝕜 (↑n) f s) (hg : ContDiffOn 𝕜 (↑n) g s) :
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)
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)
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_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)