Module docstring
{"# Composition of analytic functions
In this file we prove that the composition of analytic functions is analytic.
The argument is the following. Assume g z = ∑' qₙ (z, ..., z) and f y = ∑' pₖ (y, ..., y). Then
g (f y) = ∑' qₙ (∑' pₖ (y, ..., y), ..., ∑' pₖ (y, ..., y))
= ∑' qₙ (p_{i₁} (y, ..., y), ..., p_{iₙ} (y, ..., y)).
For each n and i₁, ..., iₙ, define a i₁ + ... + iₙ multilinear function mapping
(y₀, ..., y_{i₁ + ... + iₙ - 1}) to
qₙ (p_{i₁} (y₀, ..., y_{i₁-1}), p_{i₂} (y_{i₁}, ..., y_{i₁ + i₂ - 1}), ..., p_{iₙ} (....))).
Then g ∘ f is obtained by summing all these multilinear functions.
To formalize this, we use compositions of an integer N, i.e., its decompositions into
a sum i₁ + ... + iₙ of positive integers. Given such a composition c and two formal
multilinear series q and p, let q.compAlongComposition p c be the above multilinear
function. Then the N-th coefficient in the power series expansion of g ∘ f is the sum of these
terms over all c : Composition N.
To complete the proof, we need to show that this power series has a positive radius of convergence.
This follows from the fact that Composition N has cardinality 2^(N-1) and estimates on
the norm of qₙ and pₖ, which give summability. We also need to show that it indeed converges to
g ∘ f. For this, we note that the composition of partial sums converges to g ∘ f, and that it
corresponds to a part of the whole sum, on a subset that increases to the whole space. By
summability of the norms, this implies the overall convergence.
Main results
q.comp pis the formal composition of the formal multilinear seriesqandp.HasFPowerSeriesAt.compstates that if two functionsgandfadmit power series expansionsqandp, theng ∘ fadmits a power series expansion given byq.comp p.AnalyticAt.compstates that the composition of analytic functions is analytic.FormalMultilinearSeries.comp_assocstates that composition is associative on formal multilinear series.
Implementation details
The main technical difficulty is to write down things. In particular, we need to define precisely
q.compAlongComposition p c and to show that it is indeed a continuous multilinear
function. This requires a whole interface built on the class Composition. Once this is set,
the main difficulty is to reorder the sums, writing the composition of the partial sums as a sum
over some subset of Σ n, Composition n. We need to check that the reordering is a bijection,
running over difficulties due to the dependent nature of the types under consideration, that are
controlled thanks to the interface for Composition.
The associativity of composition on formal multilinear series is a nontrivial result: it does not
follow from the associativity of composition of analytic functions, as there is no uniqueness for
the formal multilinear series representing a function (and also, it holds even when the radius of
convergence of the series is 0). Instead, we give a direct proof, which amounts to reordering
double sums in a careful way. The change of variables is a canonical (combinatorial) bijection
Composition.sigmaEquivSigmaPi between (Σ (a : Composition n), Composition a.length) and
(Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i)), and is described
in more details below in the paragraph on associativity.
","### Composing formal multilinear series ","In this paragraph, we define the composition of formal multilinear series, by summing over all
possible compositions of n.
","### The identity formal power series
We will now define the identity power series, and show that it is a neutral element for left and right composition. ","### Summability properties of the composition of formal power series ","### Composing analytic functions
Now, we will prove that the composition of the partial sums of q and p up to order N is
given by a sum over some large subset of Σ n, Composition n of q.compAlongComposition p, to
deduce that the series for q.comp p indeed converges to g ∘ f when q is a power series for
g and p is a power series for f.
This proof is a big reindexing argument of a sum. Since it is a bit involved, we define first
the source of the change of variables (compPartialSumSource), its target
(compPartialSumTarget) and the change of variables itself (compChangeOfVariables) before
giving the main statement in comp_partialSum. ","### Associativity of the composition of formal multilinear series
In this paragraph, we prove the associativity of the composition of formal power series.
By definition,
(r.comp q).comp p n v
= ∑_{i₁ + ... + iₖ = n} (r.comp q)ₖ (p_{i₁} (v₀, ..., v_{i₁ -1}), p_{i₂} (...), ..., p_{iₖ}(...))
= ∑_{a : Composition n} (r.comp q) a.length (applyComposition p a v)
decomposing r.comp q in the same way, we get
(r.comp q).comp p n v
= ∑_{a : Composition n} ∑_{b : Composition a.length}
r b.length (applyComposition q b (applyComposition p a v))
On the other hand,
r.comp (q.comp p) n v = ∑_{c : Composition n} r c.length (applyComposition (q.comp p) c v)
Here, applyComposition (q.comp p) c v is a vector of length c.length, whose i-th term is
given by (q.comp p) (c.blocksFun i) (v_l, v_{l+1}, ..., v_{m-1}) where {l, ..., m-1} is the
i-th block in the composition c, of length c.blocksFun i by definition. To compute this term,
we expand it as ∑_{dᵢ : Composition (c.blocksFun i)} q dᵢ.length (applyComposition p dᵢ v'),
where v' = (v_l, v_{l+1}, ..., v_{m-1}). Therefore, we get
r.comp (q.comp p) n v =
∑_{c : Composition n} ∑_{d₀ : Composition (c.blocksFun 0),
..., d_{c.length - 1} : Composition (c.blocksFun (c.length - 1))}
r c.length (fun i ↦ q dᵢ.length (applyComposition p dᵢ v'ᵢ))
To show that these terms coincide, we need to explain how to reindex the sums to put them in
bijection (and then the terms we are summing will correspond to each other). Suppose we have a
composition a of n, and a composition b of a.length. Then b indicates how to group
together some blocks of a, giving altogether b.length blocks of blocks. These blocks of blocks
can be called d₀, ..., d_{a.length - 1}, and one obtains a composition c of n by saying that
each dᵢ is one single block. Conversely, if one starts from c and the dᵢs, one can concatenate
the dᵢs to obtain a composition a of n, and register the lengths of the dᵢs in a composition
b of a.length.
An example might be enlightening. Suppose a = [2, 2, 3, 4, 2]. It is a composition of
length 5 of 13. The content of the blocks may be represented as 0011222333344.
Now take b = [2, 3] as a composition of a.length = 5. It says that the first 2 blocks of a
should be merged, and the last 3 blocks of a should be merged, giving a new composition of 13
made of two blocks of length 4 and 9, i.e., c = [4, 9]. But one can also remember that
the new first block was initially made of two blocks of size 2, so d₀ = [2, 2], and the new
second block was initially made of three blocks of size 3, 4 and 2, so d₁ = [3, 4, 2].
This equivalence is called Composition.sigmaEquivSigmaPi n below.
We start with preliminary results on compositions, of a very specialized nature, then define the
equivalence Composition.sigmaEquivSigmaPi n, and we deduce finally the associativity of
composition of formal multilinear series in FormalMultilinearSeries.comp_assoc.
"}