mathlib

0bc15f82 - feat(analysis/analytic/composition): the composition of analytic functions is analytic (#2399)

feat(analysis/analytic/composition): the composition of analytic functions is analytic (#2399) 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. The main difficulty is to make sense of this (especially the ellipsis) in a way that Lean understands. For this, this PR uses a structure containing a decomposition of `n` as a sum `i_1 + ... i_k` (called `composition`), and a whole interface around it developed in #2398. Once it is available, the main proof is not too hard. This supersedes #2328, after a new start implementing compositions using sequences. Co-authored-by: Scott Morrison <scott@tqft.net>