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_0, ..., v_{n-1}) = ∑_{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.

Current state

For now, the file only contains the combinatorial construction, i.e., the definition of OrderedFinpartition n and the equivalence between (c : OrderedFinpartition n) × Option (Fin c.length) and OrderedFinpartition (n + 1). The application to the proof of the Faa di Bruno formula will be PRed in a second step.

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 : OrderedFinpartition n} {y : OrderedFinpartition n} (length : x.length = y.length) (partSize : HEq x.partSize y.partSize) (emb : HEq x.emb y.emb) : x = y

theorem OrderedFinpartition.partSize_pos {n : ℕ} (self : OrderedFinpartition n) (m : Fin self.length) : 0 < self.partSize m

theorem OrderedFinpartition.emb_strictMono {n : ℕ} (self : OrderedFinpartition n) (m : Fin self.length) : StrictMono (self.emb m)

theorem OrderedFinpartition.parts_strictMono {n : ℕ} (self : OrderedFinpartition n) : StrictMono fun (m : Fin self.length) => self.emb m ⟨self.partSize m - 1, ⋯⟩

The parts are ordered by increasing greatest element.

theorem OrderedFinpartition.disjoint {n : ℕ} (self : OrderedFinpartition n) : Set.univ.PairwiseDisjoint fun (m : Fin self.length) => Set.range (self.emb m)

The parts are disjoint

theorem OrderedFinpartition.cover {n : ℕ} (self : OrderedFinpartition n) (x : Fin n) : ∃ (m : Fin self.length), x ∈ Set.range (self.emb m)

The parts cover everything

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 : Fin c.length} {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_1} [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_1} [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 : Fin c.length) (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.