Faa di Bruno formula

The Faa di Bruno formula gives the iterated derivative of g ∘ f in terms of those of g and f. It is expressed in terms of partitions I of {0, ..., n-1}. For such a partition, denote by k its number of parts, write the parts as I₀, ..., Iₖ₋₁ ordered so that max I₀ < ... < max Iₖ₋₁, and let iₘ be the number of elements of Iₘ. Then D^n (g ∘ f) (x) (v₀, ..., vₙ₋₁) = ∑_{I partition of {0, ..., n-1}} D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁})) where by v_{Iₘ} we mean the vectors vᵢ with indices in Iₘ, i.e., the composition of v with the increasing embedding of Fin iₘ into Fin n with range Iₘ.

For instance, for n = 2, there are 2 partitions of {0, 1}, given by {0}, {1} and {0, 1}, and therefore D^2(g ∘ f) (x) (v₀, v₁) = D^2 g (f x) (Df (x) v₀, Df (x) v₁) + Dg (f x) (D^2f (x) (v₀, v₁)).

The formula is straightforward to prove by induction, as differentiating D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁})) gives a sum with k + 1 terms where one differentiates either D^k g (f x), or one of the D^{iₘ} f (x), amounting to adding to the partition I either a new atom {-1} to its left, or extending Iₘ by adding -1 to it. In this way, one obtains bijectively all partitions of {-1, ..., n}, and the proof can go on (up to relabelling).

The main difficulty is to write things down in a precise language, namely to write D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁})) as a continuous multilinear map of the vᵢ. For this, instead of working with partitions of {0, ..., n-1} and ordering their parts, we work with partitions in which the ordering is part of the data -- this is equivalent, but much more convenient to implement. We call these OrderedFinpartition n.

Note that the implementation of OrderedFinpartition is very specific to the Faa di Bruno formula: as testified by the formula above, what matters is really the embedding of the parts in Fin n, and moreover the parts have to be ordered by max I₀ < ... < max Iₖ₋₁ for the formula to hold in the general case where the iterated differential might not be symmetric. The defeqs with respect to Fin.cons are also important when doing the induction. For this reason, we do not expect this class to be useful beyond the Faa di Bruno formula, which is why it is in this file instead of a dedicated file in the Combinatorics folder.

Main results

Given c : OrderedFinpartition n and two formal multilinear series q and p, we define c.compAlongOrderedFinpartition q p as an n-multilinear map given by the formula above, i.e., (v₁, ..., vₙ) ↦ qₖ (p_{i₁} (v_{I₁}), ..., p_{iₖ} (v_{Iₖ})).

Then, we define q.taylorComp p as a formal multilinear series whose n-th term is the sum of c.compAlongOrderedFinpartition q p over all ordered finpartitions of size n.

Finally, we prove in HasFTaylorSeriesUptoOn.comp that, 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.

Implementation

A first technical difficulty is to implement the extension process of OrderedFinpartition corresponding to adding a new atom, or appending an atom to an existing part, and defining the associated increasing parameterizations that show up in the definition of compAlongOrderedFinpartition.

Then, one has to show that the ordered finpartitions thus obtained give exactly all ordered finpartitions of order n+1. For this, we define the inverse process (shrinking a finpartition of n+1 by erasing 0, either as an atom or from the part that contains it), and we show that these processes are inverse to each other, yielding an equivalence between (c : OrderedFinpartition n) × Option (Fin c.length) and OrderedFinpartition (n + 1). This equivalence shows up prominently in the inductive proof of Faa di Bruno formula to identify the sums that show up.

structure OrderedFinpartition (n : ℕ) : Type

A partition of Fin n into finitely many nonempty subsets, given by the increasing parameterization of these subsets. We order the subsets by increasing greatest element. This definition is tailored-made for the Faa di Bruno formula, and probably not useful elsewhere, because of the specific parameterization by Fin n and the peculiar ordering.

• length : ℕ

  The number of parts in the partition

• partSize : Fin self.length → ℕ

  The size of each part

• partSize_pos (m : Fin self.length) : 0 < self.partSize m
• emb (m : Fin self.length) : Fin (self.partSize m) → Fin n

  The increasing parameterization of each part

• emb_strictMono (m : Fin self.length) : StrictMono (self.emb m)
• parts_strictMono : StrictMono fun (m : Fin self.length) => self.emb m ⟨self.partSize m - 1, ⋯⟩

  The parts are ordered by increasing greatest element.

• disjoint : Set.univ.PairwiseDisjoint fun (m : Fin self.length) => Set.range (self.emb m)

  The parts are disjoint

• cover (x : Fin n) : ∃ (m : Fin self.length), x ∈ Set.range (self.emb m)

  The parts cover everything

theorem OrderedFinpartition.ext {n : ℕ} {x y : OrderedFinpartition n} (length : x.length = y.length) (partSize : HEq x.partSize y.partSize) (emb : HEq x.emb y.emb) : x = y

Basic API for ordered finpartitions

def OrderedFinpartition.atomic (n : ℕ) : OrderedFinpartition n

The ordered finpartition of Fin n into singletons.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OrderedFinpartition.atomic_length (n : ℕ) : (OrderedFinpartition.atomic n).length = n

@[simp]

theorem OrderedFinpartition.atomic_emb (n : ℕ) (m : Fin n) (x✝ : Fin ((fun (x : Fin n) => 1) m)) : (OrderedFinpartition.atomic n).emb m x✝ = m

@[simp]

theorem OrderedFinpartition.atomic_partSize (n : ℕ) (x✝ : Fin n) : (OrderedFinpartition.atomic n).partSize x✝ = 1

instance OrderedFinpartition.instInhabited {n : ℕ} : Inhabited (OrderedFinpartition n)

Equations

• OrderedFinpartition.instInhabited = { default := OrderedFinpartition.atomic n }

theorem OrderedFinpartition.length_le {n : ℕ} (c : OrderedFinpartition n) : c.length ≤ n

theorem OrderedFinpartition.partSize_le {n : ℕ} (c : OrderedFinpartition n) (m : Fin c.length) : c.partSize m ≤ n

def OrderedFinpartition.embSigma (n : ℕ) : OrderedFinpartition n → (l : Fin (n + 1)) × (p : Fin ↑l → Fin (n + 1)) × ((i : Fin ↑l) → Fin ↑(p i) → Fin n)

Embedding of ordered finpartitions in a sigma type. The sigma type on the right is quite big, but this is enough to get finiteness of ordered finpartitions.

Equations

• OrderedFinpartition.embSigma n c = ⟨⟨c.length, ⋯⟩, ⟨fun (m : Fin ↑⟨c.length, ⋯⟩) => ⟨c.partSize m, ⋯⟩, fun (j : Fin ↑⟨c.length, ⋯⟩) => c.emb j⟩⟩

theorem OrderedFinpartition.injective_embSigma (n : ℕ) : Function.Injective (OrderedFinpartition.embSigma n)

noncomputable instance OrderedFinpartition.instFintype {n : ℕ} : Fintype (OrderedFinpartition n)

Equations

• OrderedFinpartition.instFintype = Fintype.ofInjective (OrderedFinpartition.embSigma n) ⋯

instance OrderedFinpartition.instUniqueOfNatNat : Unique (OrderedFinpartition 0)

Equations

• OrderedFinpartition.instUniqueOfNatNat = Unique.mk' (OrderedFinpartition 0)

theorem OrderedFinpartition.exists_inverse {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) : ∃ (p : (m : Fin c.length) × Fin (c.partSize m)), c.emb p.fst p.snd = j

theorem OrderedFinpartition.emb_injective {n : ℕ} (c : OrderedFinpartition n) : Function.Injective fun (p : (m : Fin c.length) × Fin (c.partSize m)) => c.emb p.fst p.snd

theorem OrderedFinpartition.emb_ne_emb_of_ne {n : ℕ} (c : OrderedFinpartition n) {i j : Fin c.length} {a : Fin (c.partSize i)} {b : Fin (c.partSize j)} (h : i ≠ j) : c.emb i a ≠ c.emb j b

noncomputable def OrderedFinpartition.index {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) : Fin c.length

Given j : Fin n, the index of the part to which it belongs.

Equations

• c.index j = ⋯.choose.fst

noncomputable def OrderedFinpartition.invEmbedding {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) : Fin (c.partSize (c.index j))

The inverse of c.emb for c : OrderedFinpartition. It maps j : Fin n to the point in Fin (c.partSize (c.index j)) which is mapped back to j by c.emb (c.index j).

Equations

• c.invEmbedding j = ⋯.choose.snd

@[simp]

theorem OrderedFinpartition.emb_invEmbedding {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) : c.emb (c.index j) (c.invEmbedding j) = j

noncomputable def OrderedFinpartition.equivSigma {n : ℕ} (c : OrderedFinpartition n) : (i : Fin c.length) × Fin (c.partSize i) ≃ Fin n

An ordered finpartition gives an equivalence between Fin n and the disjoint union of the parts, each of them parameterized by Fin (c.partSize i).

Equations

• c.equivSigma = { toFun := fun (p : (i : Fin c.length) × Fin (c.partSize i)) => c.emb p.fst p.snd, invFun := fun (i : Fin n) => ⟨c.index i, c.invEmbedding i⟩, left_inv := ⋯, right_inv := ⋯ }

theorem OrderedFinpartition.prod_sigma_eq_prod {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [CommMonoid α] (v : Fin n → α) : ∏ m : Fin c.length, ∏ r : Fin (c.partSize m), v (c.emb m r) = ∏ i : Fin n, v i

theorem OrderedFinpartition.sum_sigma_eq_sum {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [AddCommMonoid α] (v : Fin n → α) : ∑ m : Fin c.length, ∑ r : Fin (c.partSize m), v (c.emb m r) = ∑ i : Fin n, v i

theorem OrderedFinpartition.length_pos {n : ℕ} (c : OrderedFinpartition n) (h : 0 < n) : 0 < c.length

theorem OrderedFinpartition.neZero_length {n : ℕ} [NeZero n] (c : OrderedFinpartition n) : NeZero c.length

theorem OrderedFinpartition.neZero_partSize {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : NeZero (c.partSize i)

theorem OrderedFinpartition.emb_zero {n : ℕ} (c : OrderedFinpartition n) [NeZero n] : c.emb (c.index 0) 0 = 0

theorem OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton {n : ℕ} (c : OrderedFinpartition n) {i : Fin c.length} {j : Fin n} (hc : Set.range (c.emb i) = {j}) : c.partSize i = 1

theorem OrderedFinpartition.one_lt_partSize_index_zero {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) ≠ {0}) : 1 < c.partSize (c.index 0)

If the left-most part is not {0}, then the part containing 0 has at least two elements: either because it's the left-most part, and then it's not just 0 by assumption, or because it's not the left-most part and then, by increasingness of maximal elements in parts, it contains a positive element.

Extending and shrinking ordered finpartitions

We show how an ordered finpartition can be extended to the left, either by adding a new atomic part (in extendLeft) or adding the new element to an existing part (in extendMiddle). Conversely, one can shrink a finpartition by deleting the element to the left, with a different behavior if it was an atomic part (in eraseLeft, in which case the number of parts decreases by one) or if it belonged to a non-atomic part (in eraseMiddle, in which case the number of parts stays the same).

These operations are inverse to each other, giving rise to an equivalence between ((c : OrderedFinpartition n) × Option (Fin c.length)) and OrderedFinpartition (n + 1) called OrderedFinPartition.extendEquiv.

def OrderedFinpartition.extendLeft {n : ℕ} (c : OrderedFinpartition n) : OrderedFinpartition (n + 1)

Extend an ordered partition of n entries, by adding a new singleton part to the left.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OrderedFinpartition.range_extendLeft_zero {n : ℕ} (c : OrderedFinpartition n) : Set.range (c.extendLeft.emb 0) = {0}

def OrderedFinpartition.extendMiddle {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length) : OrderedFinpartition (n + 1)

Extend an ordered partition of n entries, by adding to the i-th part a new point to the left.

Equations

• One or more equations did not get rendered due to their size.

theorem OrderedFinpartition.index_extendMiddle_zero {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : (c.extendMiddle i).index 0 = i

theorem OrderedFinpartition.range_emb_extendMiddle_ne_singleton_zero {n : ℕ} (c : OrderedFinpartition n) (i j : Fin c.length) : Set.range ((c.extendMiddle i).emb j) ≠ {0}

def OrderedFinpartition.extend {n : ℕ} (c : OrderedFinpartition n) (i : Option (Fin c.length)) : OrderedFinpartition (n + 1)

Extend an ordered partition of n entries, by adding singleton to the left or appending it to one of the existing part.

Equations

• c.extend none = c.extendLeft
• c.extend (some i_2) = c.extendMiddle i_2

def OrderedFinpartition.eraseLeft {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) = {0}) : OrderedFinpartition n

Given an ordered finpartition of n+1, with a leftmost atom equal to {0}, remove this atom to form an ordered finpartition of n.

Equations

• One or more equations did not get rendered due to their size.

def OrderedFinpartition.eraseMiddle {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) ≠ {0}) : OrderedFinpartition n

Given an ordered finpartition of n+1, with a leftmost atom different from {0}, remove {0} from the atom that contains it, to form an ordered finpartition of n.

Equations

• One or more equations did not get rendered due to their size.

def OrderedFinpartition.extendEquiv (n : ℕ) : (c : OrderedFinpartition n) × Option (Fin c.length) ≃ OrderedFinpartition (n + 1)

Extending the ordered partitions of Fin n bijects with the ordered partitions of Fin (n+1).

Equations

• One or more equations did not get rendered due to their size.

Applying ordered finpartitions to multilinear maps

def OrderedFinpartition.applyOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) : (Fin n → E) → Fin c.length → F

Given a formal multilinear series p, an ordered partition c of n and the index i of a block of c, we may define a function on Fin n → E by picking the variables in the i-th block of n, and applying the corresponding coefficient of p to these variables. This function is called p.applyOrderedFinpartition c v i for v : Fin n → E and i : Fin c.k.

Equations

• c.applyOrderedFinpartition p v m = (p m) (v ∘ c.emb m)

theorem OrderedFinpartition.applyOrderedFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) : c.applyOrderedFinpartition p v = fun (m : Fin c.length) => (p m) (v ∘ c.emb m)

theorem OrderedFinpartition.norm_applyOrderedFinpartition_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) (m : Fin c.length) : ‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i : Fin (c.partSize m), ‖v (c.emb m i)‖

theorem OrderedFinpartition.applyOrderedFinpartition_update_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (j : Fin n) (v : Fin n → E) (z : E) : c.applyOrderedFinpartition p (Function.update v j z) = Function.update (c.applyOrderedFinpartition p v) (c.index j) ((p (c.index j)) (Function.update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))

Technical lemma stating how c.applyOrderedFinpartition commutes with updating variables. This will be the key point to show that functions constructed from applyOrderedFinpartition retain multilinearity.

theorem OrderedFinpartition.applyOrderedFinpartition_update_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (m : Fin c.length) (v : Fin n → E) (q : ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize m)) => E) F) : c.applyOrderedFinpartition (Function.update p m q) v = Function.update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))

def OrderedFinpartition.compAlongOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G

Given a an ordered finite partition c of n, a continuous multilinear map f in c.length variables, and for each m a continuous multilinear map p m in c.partSize m variables, one can form a continuous multilinear map in n variables by applying p m to each part of the partition, and then applying f to the resulting vector. It is called c.compAlongOrderedFinpartition f p.

Equations

• c.compAlongOrderedFinpartition f p = { toFun := fun (v : Fin n → E) => f (c.applyOrderedFinpartition p v), map_update_add' := ⋯, map_update_smul' := ⋯, cont := ⋯ }

@[simp]

theorem OrderedFinpartition.compAlongOrderFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) : (c.compAlongOrderedFinpartition f p) v = f (c.applyOrderedFinpartition p v)

theorem OrderedFinpartition.norm_compAlongOrderedFinpartition_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) : ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

def OrderedFinpartition.compAlongOrderedFinpartitionₗ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G →ₗ[𝕜] MultilinearMap 𝕜 (fun (i : Fin c.length) => ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G)

Bundled version of compAlongOrderedFinpartition, depending linearly on f and multilinearly on p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) : (c.compAlongOrderedFinpartitionₗ f) p = c.compAlongOrderedFinpartition f p

noncomputable def OrderedFinpartition.compAlongOrderedFinpartitionL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (G : Type u_4) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G)

Bundled version of compAlongOrderedFinpartition, depending continuously linearly on f and continuously multilinearly on p.

Equations

• OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c = MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 ⋯

@[simp]

theorem OrderedFinpartition.compAlongOrderedFinpartitionL_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) : ((OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c) f) p = c.compAlongOrderedFinpartition f p

theorem OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) : ‖OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c‖ ≤ 1

The Faa di Bruno formula

def FormalMultilinearSeries.compAlongOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G

Given two formal multilinear series q and p and a composition c of n, one may form a continuous multilinear map in n variables by applying the right coefficient of p to each block of the composition, and then applying q c.length to the resulting vector. It is called q.compAlongComposition p c.

Equations

• q.compAlongOrderedFinpartition p c = c.compAlongOrderedFinpartition (q c.length) fun (m : Fin c.length) => p (c.partSize m)

@[simp]

theorem FormalMultilinearSeries.compAlongOrderedFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) (v : Fin n → E) : (q.compAlongOrderedFinpartition p c) v = (q c.length) (c.applyOrderedFinpartition (fun (m : Fin c.length) => p (c.partSize m)) v)

noncomputable def FormalMultilinearSeries.taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E G

Taylor formal composition of two formal multilinear series. The n-th coefficient in the composition is defined to be the sum of q.compAlongOrderedFinpartition p c over all ordered partitions of n. In other words, this term (as a multilinear function applied to v₀, ..., vₙ₋₁) is ∑'_{k} ∑'_{I₀ ⊔ ... ⊔ Iₖ₋₁ = {0, ..., n-1}} qₖ (p_{i₀} (...), ..., p_{iₖ₋₁} (...)), where iₘ is the size of Iₘ and one puts all variables of Iₘ as arguments to p_{iₘ}, in increasing order. The sets I₀, ..., Iₖ₋₁ are ordered so that max I₀ < max I₁ < ... < max Iₖ₋₁.

This definition is chosen so that the n-th derivative of g ∘ f is the Taylor composition of the iterated derivatives of g and of f.

Not to be confused with another notion of composition for formal multilinear series, called just FormalMultilinearSeries.comp, appearing in the composition of analytic functions.

Equations

• q.taylorComp p n = ∑ c : OrderedFinpartition n, q.compAlongOrderedFinpartition p c

theorem analyticOn_taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {t : Set F} {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F} (hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun (x : F) => q x n) t) (hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun (x : E) => p x n) s) {f : E → F} (hf : AnalyticOn 𝕜 f s) (h : Set.MapsTo f s t) (n : ℕ) : AnalyticOn 𝕜 (fun (x : E) => (q (f x)).taylorComp (p x) n) s

theorem HasFTaylorSeriesUpToOn.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {t : Set F} {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {g : F → G} {f : E → F} (hg : HasFTaylorSeriesUpToOn n g q t) (hf : HasFTaylorSeriesUpToOn n f p s) (h : Set.MapsTo f s t) : HasFTaylorSeriesUpToOn n (g ∘ f) (fun (x : E) => (q (f x)).taylorComp (p x)) s

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.