English
The composition map equals the sum over partitions applied blockwise, i.e., q.taylorComp p is the sum over applicable partitions of q.compAlongOrderedFinpartition p.
Русский
Композиция равна сумме по разбиениям, применяемым к каждому блоку: q.taylorComp p — сумма по допустимым разбиениям от q.compAlongOrderedFinpartition p.
LaTeX
$$q.taylorComp p = (fun n ↦ ∑ c : OrderedFinpartition n, q.compAlongOrderedFinpartition p c)$$
Lean4
/-- *Faa di Bruno* formula: If two functions `g` and `f` have Taylor series up to `n` given by
`q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`. -/
theorem comp {n : WithTop ℕ∞} {g : F → G} {f : E → F} (hg : HasFTaylorSeriesUpToOn n g q t)
(hf : HasFTaylorSeriesUpToOn n f p s) (h : MapsTo f s t) :
HasFTaylorSeriesUpToOn n (g ∘ f) (fun x ↦ (q (f x)).taylorComp (p x)) s := by
/- One has to check that the `m+1`-th term is the derivative of the `m`-th term. The `m`-th term
is a sum, that one can differentiate term by term. Each term is a linear map into continuous
multilinear maps, applied to parts of `p` and `q`. One knows how to differentiate such a map,
thanks to `HasFDerivWithinAt.linear_multilinear_comp`. The terms that show up are matched, using
`faaDiBruno_aux1` and `faaDiBruno_aux2`, with terms of the same form at order `m+1`. Then, one
needs to check that one gets each term once and exactly once, which is given by the bijection
`OrderedFinpartition.extendEquiv m`. -/
classical
constructor
· intro x hx
simp [FormalMultilinearSeries.taylorComp, default, HasFTaylorSeriesUpToOn.zero_eq' hg (h hx)]
· intro m hm x hx
have A (c : OrderedFinpartition m) :
HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
(∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x :=
by
let B := c.compAlongOrderedFinpartitionL 𝕜 E F G
change
HasFDerivWithinAt (fun y ↦ B (q (f y) c.length) (fun i ↦ p y (c.partSize i)))
(∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
have cm : (c.length : WithTop ℕ∞) ≤ m := mod_cast OrderedFinpartition.length_le c
have cp i : (c.partSize i : WithTop ℕ∞) ≤ m := by exact_mod_cast OrderedFinpartition.partSize_le c i
have I i : HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x :=
hf.fderivWithin (c.partSize i) ((cp i).trans_lt hm) x hx
have J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft t (f x) :=
hg.fderivWithin c.length (cm.trans_lt hm) (f x) (h hx)
have K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x :=
hf.hasFDerivWithinAt (le_trans (mod_cast Nat.le_add_left 1 m) (ENat.add_one_natCast_le_withTop_of_lt hm)) hx
convert HasFDerivWithinAt.linear_multilinear_comp (J.comp x K h) I B
simp only [B, Nat.succ_eq_add_one, Fintype.sum_option, comp_apply, faaDiBruno_aux1, faaDiBruno_aux2]
have B :
HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
(∑ c : OrderedFinpartition m,
∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft)
s x :=
HasFDerivWithinAt.fun_sum (fun c _ ↦ A c)
suffices
∑ c : OrderedFinpartition m,
∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)) =
(q (f x)).taylorComp (p x) (m + 1)
by
rw [← this]
convert B
ext v
simp only [Nat.succ_eq_add_one, Fintype.sum_option, ContinuousMultilinearMap.curryLeft_apply,
ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.add_apply,
FormalMultilinearSeries.compAlongOrderedFinpartition_apply, ContinuousLinearMap.coe_sum', Finset.sum_apply,
ContinuousLinearMap.add_apply]
rw [Finset.sum_sigma']
exact Fintype.sum_equiv (OrderedFinpartition.extendEquiv m) _ _ (fun p ↦ rfl)
· intro m hm
apply continuousOn_finset_sum _ (fun c _ ↦ ?_)
let B := c.compAlongOrderedFinpartitionL 𝕜 E F G
change ContinuousOn ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun i ↦ p x (c.partSize i)))) s
apply B.continuous_uncurry_of_multilinear.comp_continuousOn (ContinuousOn.prodMk ?_ ?_)
· have : (c.length : WithTop ℕ∞) ≤ m := mod_cast OrderedFinpartition.length_le c
exact (hg.cont c.length (this.trans hm)).comp hf.continuousOn h
· apply continuousOn_pi.2 (fun i ↦ ?_)
have : (c.partSize i : WithTop ℕ∞) ≤ m := by exact_mod_cast OrderedFinpartition.partSize_le c i
exact hf.cont _ (this.trans hm)
