Commit 2020-04-17 09:39 0bc15f82
View on Github →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.