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_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)
:
iteratedDerivWithin n (f + g) s x = 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 𝕜}
(h : UniqueDiffOn 𝕜 s)
{f : 𝕜 → F}
{g : 𝕜 → F}
(hfg : Set.EqOn f g s)
:
Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n g s) 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)
:
iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
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}
(hf : ContDiffOn 𝕜 (↑n) f s)
:
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}
(hf : ContDiffOn 𝕜 (↑n) f s)
:
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)
:
iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s 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)
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)