# 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.comp_along_composition 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 p`

is the formal composition of the formal multilinear series`q`

and`p`

.`has_fpower_series_at.comp`

states that if two functions`g`

and`f`

admit power series expansions`q`

and`p`

, then`g ∘ f`

admits a power series expansion given by`q.comp p`

.`analytic_at.comp`

states that the composition of analytic functions is analytic.`FormalMultilinearSeries.comp_assoc`

states 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.comp_along_composition 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.sigma_equiv_sigma_pi`

between `(Σ (a : composition n), composition a.length)`

and
`(Σ (c : composition n), Π (i : fin c.length), composition (c.blocks_fun 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`

.

Given a formal multilinear series `p`

, a composition `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.apply_composition c v i`

for `v : fin n → E`

and `i : fin c.length`

.

## Equations

- FormalMultilinearSeries.applyComposition p c v i = (p (Composition.blocksFun c i)) (v ∘ ⇑(Composition.embedding c i))

## Instances For

Technical lemma stating how `p.apply_composition`

commutes with updating variables. This
will be the key point to show that functions constructed from `apply_composition`

retain
multilinearity.

Given a formal multilinear series `p`

, a composition `c`

of `n`

and a continuous multilinear
map `f`

in `c.length`

variables, 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 `f`

to
the resulting vector. It is called `f.comp_along_composition p c`

.

## Equations

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

## Instances For

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.comp_along_composition p c`

.

## Equations

## Instances For

Formal composition of two formal multilinear series. The `n`

-th coefficient in the composition
is defined to be the sum of `q.comp_along_composition p c`

over all compositions of
`n`

. In other words, this term (as a multilinear function applied to `v_0, ..., v_{n-1}`

) is
`∑'_{k} ∑'_{i₁ + ... + iₖ = n} qₖ (p_{i_1} (...), ..., p_{i_k} (...))`

, where one puts all variables
`v_0, ..., v_{n-1}`

in increasing order in the dots.

In general, the composition `q ∘ p`

only makes sense when the constant coefficient of `p`

vanishes.
We give a general formula but which ignores the value of `p 0`

instead.

## Equations

- FormalMultilinearSeries.comp q p n = Finset.sum Finset.univ fun (c : Composition n) => FormalMultilinearSeries.compAlongComposition q p c

## Instances For

The `0`

-th coefficient of `q.comp p`

is `q 0`

. Since these maps are multilinear maps in zero
variables, but on different spaces, we can not state this directly, so we state it when applied to
arbitrary vectors (which have to be the zero vector).

The `0`

-th coefficient of `q.comp p`

is `q 0`

. When `p`

goes from `E`

to `E`

, this can be
expressed as a direct equality

The first coefficient of a composition of formal multilinear series is the composition of the first coefficients seen as continuous linear maps.

Only `0`

-th coefficient of `q.comp p`

depends on `q 0`

.

The norm of `f.comp_along_composition p c`

is controlled by the product of
the norms of the relevant bits of `f`

and `p`

.

The norm of `q.comp_along_composition p c`

is controlled by the product of
the norms of the relevant bits of `q`

and `p`

.

### 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.

The identity formal multilinear series, with all coefficients equal to `0`

except for `n = 1`

where it is (the continuous multilinear version of) the identity.

## Equations

- FormalMultilinearSeries.id 𝕜 E x = match x with | 0 => 0 | 1 => (LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E E)) (ContinuousLinearMap.id 𝕜 E) | x => 0

## Instances For

The first coefficient of `id 𝕜 E`

is the identity.

The `n`

th coefficient of `id 𝕜 E`

is the identity when `n = 1`

. We state this in a dependent
way, as it will often appear in this form.

For `n ≠ 1`

, the `n`

-th coefficient of `id 𝕜 E`

is zero, by definition.

### Summability properties of the composition of formal power series #

If two formal multilinear series have positive radius of convergence, then the terms appearing in the definition of their composition are also summable (when multiplied by a suitable positive geometric term).

Bounding below the radius of the composition of two formal multilinear series assuming summability over all compositions.

### 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.comp_along_composition 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 (`comp_partial_source`

), its target
(`comp_partial_target`

) and the change of variables itself (`comp_change_of_variables`

) before
giving the main statement in `comp_partial_sum`

.

Source set in the change of variables to compute the composition of partial sums of formal
power series.
See also `comp_partial_sum`

.

## Equations

- FormalMultilinearSeries.compPartialSumSource m M N = Finset.sigma (Finset.Ico m M) fun (n : ℕ) => Fintype.piFinset fun (_i : Fin n) => Finset.Ico 1 N

## Instances For

Change of variables appearing to compute the composition of partial sums of formal power series

## Equations

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

## Instances For

Target set in the change of variables to compute the composition of partial sums of formal power series, here given a a set.

## Equations

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

## Instances For

Target set in the change of variables to compute the composition of partial sums of formal
power series, here given a a finset.
See also `comp_partial_sum`

.

## Equations

## Instances For

`comp_change_of_variables m M N`

is a bijection between `comp_partial_sum_source m M N`

and `comp_partial_sum_target m M N`

, yielding equal sums for functions that correspond to each
other under the bijection. As `comp_change_of_variables m M N`

is a dependent function, stating
that it is a bijection is not directly possible, but the consequence on sums can be stated
more easily.

The auxiliary set corresponding to the composition of partial sums asymptotically contains all possible compositions.

Composing the partial sums of two multilinear series coincides with the sum over all
compositions in `comp_partial_sum_target 0 N N`

. This is precisely the motivation for the
definition of `comp_partial_sum_target`

.

If two functions `g`

and `f`

have power series `q`

and `p`

respectively at `f x`

and `x`

, then
`g ∘ f`

admits the power series `q.comp p`

at `x`

.

If two functions `g`

and `f`

are analytic respectively at `f x`

and `x`

, then `g ∘ f`

is
analytic at `x`

.

If two functions `g`

and `f`

are analytic respectively on `s.image f`

and `s`

, then `g ∘ f`

is
analytic on `s`

.

### 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 (apply_composition 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 (apply_composition q b (apply_composition p a v))
```

On the other hand,

```
r.comp (q.comp p) n v = ∑_{c : composition n} r c.length (apply_composition (q.comp p) c v)
```

Here, `apply_composition (q.comp p) c v`

is a vector of length `c.length`

, whose `i`

-th term is
given by `(q.comp p) (c.blocks_fun 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.blocks_fun i`

by definition. To compute this term,
we expand it as `∑_{dᵢ : composition (c.blocks_fun i)} q dᵢ.length (apply_composition 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.blocks_fun 0),
..., d_{c.length - 1} : composition (c.blocks_fun (c.length - 1))}
r c.length (λ i, q dᵢ.length (apply_composition 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.sigma_equiv_sigma_pi 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`

.

Rewriting equality in the dependent type `Σ (a : composition n), composition a.length)`

in
non-dependent terms with lists, requiring that the blocks coincide.

Rewriting equality in the dependent type
`Σ (c : composition n), Π (i : fin c.length), composition (c.blocks_fun i)`

in
non-dependent terms with lists, requiring that the lists of blocks coincide.

When `a`

is a composition of `n`

and `b`

is a composition of `a.length`

, `a.gather b`

is the
composition of `n`

obtained by gathering all the blocks of `a`

corresponding to a block of `b`

.
For instance, if `a = [6, 5, 3, 5, 2]`

and `b = [2, 3]`

, one should gather together
the first two blocks of `a`

and its last three blocks, giving `a.gather b = [11, 10]`

.

## Equations

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

## Instances For

An auxiliary function used in the definition of `sigmaEquivSigmaPi`

below, associating to
two compositions `a`

of `n`

and `b`

of `a.length`

, and an index `i`

bounded by the length of
`a.gather b`

, the subcomposition of `a`

made of those blocks belonging to the `i`

-th block of
`a.gather b`

.

## Equations

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

## Instances For

Auxiliary lemma to prove that the composition of formal multilinear series is associative.

Consider a composition `a`

of `n`

and a composition `b`

of `a.length`

. Grouping together some
blocks of `a`

according to `b`

as in `a.gather b`

, one can compute the total size of the blocks
of `a`

up to an index `size_up_to b i + j`

(where the `j`

corresponds to a set of blocks of `a`

that do not fill a whole block of `a.gather b`

). The first part corresponds to a sum of blocks
in `a.gather b`

, and the second one to a sum of blocks in the next block of
`sigma_composition_aux a b`

. This is the content of this lemma.

Natural equivalence between `(Σ (a : composition n), composition a.length)`

and
`(Σ (c : composition n), Π (i : fin c.length), composition (c.blocks_fun i))`

, that shows up as a
change of variables in the proof that composition of formal multilinear series is associative.

Consider 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. The map `⟨a, b⟩ → ⟨c, (d₀, ..., d_{a.length - 1})⟩`

is
the direct map in the equiv.

Conversely, if one starts from `c`

and the `dᵢ`

s, one can join 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`

. This is the
inverse map of the equiv.

## Equations

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