Iterated derivatives of compositions #
In this file we specialize Faà di Bruno's formula to one-dimensional domain
to deduce formulae for iteratedDerivWithin k (g ∘ f) s x for k = 2 and k = 3.
We use
vcompfor lemmas about the composition ofg : E → Fwithf : 𝕜 → E;scompfor lemmas about the composition ofg : 𝕜 → Ewithf : 𝕜 → 𝕜;compfor lemmas about the composition ofg : 𝕜 → 𝕜withf : 𝕜 → 𝕜.
TODO #
- What
UniqueDiffOnassumptions can be discarded? - In case of dimension 1 (and, more generally, in case of symmetric iterated derivatives), some terms are equal. Add versions of Faà di Bruno's formula that take the symmetries into account.
- Can we generalize
scomp/comptof : 𝕜 → 𝕜', where𝕜'is a normed algebra over𝕜? E.g.,𝕜 = ℝ,𝕜' = ℂ.
Before starting to work on these TODOs, please contact Yury Kudryashov who may have partial progress towards some of them.
theorem
iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{s : Set 𝕜}
{t : Set E}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
(hi : ↑i ≤ n)
:
iteratedDerivWithin i (g ∘ f) s x = ∑ c : OrderedFinpartition i,
(iteratedFDerivWithin 𝕜 c.length g t (f x)) fun (j : Fin c.length) => iteratedDerivWithin (c.partSize j) f s x
theorem
iteratedDeriv_vcomp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
(hi : ↑i ≤ n)
:
iteratedDeriv i (g ∘ f) x = ∑ c : OrderedFinpartition i,
(iteratedFDeriv 𝕜 c.length g (f x)) fun (j : Fin c.length) => iteratedDeriv (c.partSize j) f x
theorem
iteratedDerivWithin_vcomp_two
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{s : Set 𝕜}
{t : Set E}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 2 g t (f x))
(hf : ContDiffWithinAt 𝕜 2 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 2 (g ∘ f) s x = ((iteratedFDerivWithin 𝕜 2 g t (f x)) fun (x_1 : Fin 2) => derivWithin f s x) + (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 2 f s x)
theorem
iteratedDeriv_vcomp_two
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{x : 𝕜}
(hg : ContDiffAt 𝕜 2 g (f x))
(hf : ContDiffAt 𝕜 2 f x)
:
iteratedDeriv 2 (g ∘ f) x = ((iteratedFDeriv 𝕜 2 g (f x)) fun (x_1 : Fin 2) => deriv f x) + (fderiv 𝕜 g (f x)) (iteratedDeriv 2 f x)
theorem
iteratedDerivWithin_vcomp_three
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{s : Set 𝕜}
{t : Set E}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 3 g t (f x))
(hf : ContDiffWithinAt 𝕜 3 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 3 (g ∘ f) s x = ((iteratedFDerivWithin 𝕜 3 g t (f x)) fun (x_1 : Fin 3) => derivWithin f s x) + (iteratedFDerivWithin 𝕜 2 g t (f x)) ![iteratedDerivWithin 2 f s x, derivWithin f s x] + 2 • (iteratedFDerivWithin 𝕜 2 g t (f x)) ![derivWithin f s x, iteratedDerivWithin 2 f s x] + (fderivWithin 𝕜 g t (f x)) (iteratedDerivWithin 3 f s x)
theorem
iteratedDeriv_vcomp_three
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{g : E → F}
{f : 𝕜 → E}
{x : 𝕜}
(hg : ContDiffAt 𝕜 3 g (f x))
(hf : ContDiffAt 𝕜 3 f x)
:
iteratedDeriv 3 (g ∘ f) x = ((iteratedFDeriv 𝕜 3 g (f x)) fun (x_1 : Fin 3) => deriv f x) + (iteratedFDeriv 𝕜 2 g (f x)) ![iteratedDeriv 2 f x, deriv f x] + 2 • (iteratedFDeriv 𝕜 2 g (f x)) ![deriv f x, iteratedDeriv 2 f x] + (fderiv 𝕜 g (f x)) (iteratedDeriv 3 f x)
theorem
iteratedDerivWithin_scomp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
(hi : ↑i ≤ n)
:
iteratedDerivWithin i (g ∘ f) s x = ∑ c : OrderedFinpartition i,
(∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x) • iteratedDerivWithin c.length g t (f x)
theorem
iteratedDeriv_scomp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
(hi : ↑i ≤ n)
:
iteratedDeriv i (g ∘ f) x = ∑ c : OrderedFinpartition i, (∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x) • iteratedDeriv c.length g (f x)
theorem
iteratedDerivWithin_scomp_two
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 2 g t (f x))
(hf : ContDiffWithinAt 𝕜 2 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 2 (g ∘ f) s x = derivWithin f s x ^ 2 • iteratedDerivWithin 2 g t (f x) + iteratedDerivWithin 2 f s x • derivWithin g t (f x)
theorem
iteratedDeriv_scomp_two
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{x : 𝕜}
(hg : ContDiffAt 𝕜 2 g (f x))
(hf : ContDiffAt 𝕜 2 f x)
:
iteratedDeriv 2 (g ∘ f) x = deriv f x ^ 2 • iteratedDeriv 2 g (f x) + iteratedDeriv 2 f x • deriv g (f x)
theorem
iteratedDerivWithin_scomp_three
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 3 g t (f x))
(hf : ContDiffWithinAt 𝕜 3 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 3 (g ∘ f) s x = derivWithin f s x ^ 3 • iteratedDerivWithin 3 g t (f x) + 3 • iteratedDerivWithin 2 f s x • derivWithin f s x • iteratedDerivWithin 2 g t (f x) + iteratedDerivWithin 3 f s x • derivWithin g t (f x)
theorem
iteratedDeriv_scomp_three
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{g : 𝕜 → E}
{f : 𝕜 → 𝕜}
{x : 𝕜}
(hg : ContDiffAt 𝕜 3 g (f x))
(hf : ContDiffAt 𝕜 3 f x)
:
iteratedDeriv 3 (g ∘ f) x = deriv f x ^ 3 • iteratedDeriv 3 g (f x) + 3 • iteratedDeriv 2 f x • deriv f x • iteratedDeriv 2 g (f x) + iteratedDeriv 3 f x • deriv g (f x)
theorem
iteratedDerivWithin_comp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
(hi : ↑i ≤ n)
:
iteratedDerivWithin i (g ∘ f) s x = ∑ c : OrderedFinpartition i,
iteratedDerivWithin c.length g t (f x) * ∏ j : Fin c.length, iteratedDerivWithin (c.partSize j) f s x
theorem
iteratedDeriv_comp_eq_sum_orderedFinpartition
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{x : 𝕜}
{n : WithTop ℕ∞}
{i : ℕ}
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
(hi : ↑i ≤ n)
:
iteratedDeriv i (g ∘ f) x = ∑ c : OrderedFinpartition i, iteratedDeriv c.length g (f x) * ∏ j : Fin c.length, iteratedDeriv (c.partSize j) f x
theorem
iteratedDerivWithin_comp_two
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 2 g t (f x))
(hf : ContDiffWithinAt 𝕜 2 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 2 (g ∘ f) s x = iteratedDerivWithin 2 g t (f x) * derivWithin f s x ^ 2 + derivWithin g t (f x) * iteratedDerivWithin 2 f s x
theorem
iteratedDeriv_comp_two
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{x : 𝕜}
(hg : ContDiffAt 𝕜 2 g (f x))
(hf : ContDiffAt 𝕜 2 f x)
:
iteratedDeriv 2 (g ∘ f) x = iteratedDeriv 2 g (f x) * deriv f x ^ 2 + deriv g (f x) * iteratedDeriv 2 f x
theorem
iteratedDerivWithin_comp_three
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{s t : Set 𝕜}
{x : 𝕜}
(hg : ContDiffWithinAt 𝕜 3 g t (f x))
(hf : ContDiffWithinAt 𝕜 3 f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
:
iteratedDerivWithin 3 (g ∘ f) s x = iteratedDerivWithin 3 g t (f x) * derivWithin f s x ^ 3 + 3 * iteratedDerivWithin 2 g t (f x) * iteratedDerivWithin 2 f s x * derivWithin f s x + derivWithin g t (f x) * iteratedDerivWithin 3 f s x
theorem
iteratedDeriv_comp_three
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{g f : 𝕜 → 𝕜}
{x : 𝕜}
(hg : ContDiffAt 𝕜 3 g (f x))
(hf : ContDiffAt 𝕜 3 f x)
:
iteratedDeriv 3 (g ∘ f) x = iteratedDeriv 3 g (f x) * deriv f x ^ 3 + 3 * iteratedDeriv 2 g (f x) * iteratedDeriv 2 f x * deriv f x + deriv g (f x) * iteratedDeriv 3 f x