Module docstring
{"# 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.
","### Basic API for ordered finpartitions ","### 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.
","### Applying ordered finpartitions to multilinear maps ","### The Faa di Bruno formula "}