Documentation

Mathlib.Analysis.Analytic.Composition

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 #

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.

def FormalMultilinearSeries.applyComposition {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : } (c : Composition n) :
(Fin nE)Fin c.lengthF

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.applyComposition c v i for v : Fin n → E and i : Fin c.length.

Equations
  • p.applyComposition c v i = (p (c.blocksFun i)) (v (c.embedding i))
Instances For
    theorem FormalMultilinearSeries.applyComposition_ones {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ) :
    p.applyComposition (Composition.ones n) = fun (v : Fin nE) (i : Fin (Composition.ones n).length) => (p 1) fun (x : Fin 1) => v (Fin.castLE i)
    theorem FormalMultilinearSeries.applyComposition_single {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : } (hn : 0 < n) (v : Fin nE) :
    p.applyComposition (Composition.single n hn) v = fun (_j : Fin (Composition.single n hn).length) => (p n) v
    @[simp]
    theorem FormalMultilinearSeries.removeZero_applyComposition {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : } (c : Composition n) :
    p.removeZero.applyComposition c = p.applyComposition c
    theorem FormalMultilinearSeries.applyComposition_update {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : } (c : Composition n) (j : Fin n) (v : Fin nE) (z : E) :
    p.applyComposition c (Function.update v j z) = Function.update (p.applyComposition c v) (c.index j) ((p (c.blocksFun (c.index j))) (Function.update (v (c.embedding (c.index j))) (c.invEmbedding j) z))

    Technical lemma stating how p.applyComposition commutes with updating variables. This will be the key point to show that functions constructed from applyComposition retain multilinearity.

    @[simp]
    theorem FormalMultilinearSeries.compContinuousLinearMap_applyComposition {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] {n : } (p : FormalMultilinearSeries 𝕜 F G) (f : E →L[𝕜] F) (c : Composition n) (v : Fin nE) :
    (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (f v)
    def ContinuousMultilinearMap.compAlongComposition {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {n : } (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (f : ContinuousMultilinearMap 𝕜 (fun (_i : Fin c.length) => F) G) :
    ContinuousMultilinearMap 𝕜 (fun (_i : Fin n) => E) G

    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.compAlongComposition p c.

    Equations
    Instances For
      @[simp]
      theorem ContinuousMultilinearMap.compAlongComposition_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {n : } (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (f : ContinuousMultilinearMap 𝕜 (fun (_i : Fin c.length) => F) G) (v : Fin nE) :
      (ContinuousMultilinearMap.compAlongComposition p c f) v = f (p.applyComposition c v)

      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.compAlongComposition p c.

      Equations
      Instances For
        @[simp]
        theorem FormalMultilinearSeries.compAlongComposition_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] {n : } (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (v : Fin nE) :
        (q.compAlongComposition p c) v = (q c.length) (p.applyComposition c v)

        Formal composition of two formal multilinear series. The n-th coefficient in the composition is defined to be the sum of q.compAlongComposition 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
        • q.comp p n = c : Composition n, q.compAlongComposition p c
        Instances For
          theorem FormalMultilinearSeries.comp_coeff_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0E) (v' : Fin 0F) :
          (q.comp p 0) v = (q 0) v'

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

          @[simp]
          theorem FormalMultilinearSeries.comp_coeff_zero' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 0E) :
          (q.comp p 0) v = (q 0) fun (_i : Fin 0) => 0
          theorem FormalMultilinearSeries.comp_coeff_zero'' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (q : FormalMultilinearSeries 𝕜 E F) (p : FormalMultilinearSeries 𝕜 E E) :
          q.comp p 0 = q 0

          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

          theorem FormalMultilinearSeries.comp_coeff_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (v : Fin 1E) :
          (q.comp p 1) v = (q 1) fun (_i : Fin 1) => (p 1) v

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

          theorem FormalMultilinearSeries.removeZero_comp_of_pos {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) {n : } (hn : 0 < n) :
          q.removeZero.comp p n = q.comp p n

          Only 0-th coefficient of q.comp p depends on q 0.

          @[simp]
          theorem FormalMultilinearSeries.comp_removeZero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommRing 𝕜] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [TopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
          q.comp p.removeZero = q.comp p
          theorem FormalMultilinearSeries.compAlongComposition_bound {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : } (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) (f : ContinuousMultilinearMap 𝕜 (fun (_i : Fin c.length) => F) G) (v : Fin nE) :
          (ContinuousMultilinearMap.compAlongComposition p c f) v (f * i : Fin c.length, p (c.blocksFun i)) * i : Fin n, v i

          The norm of f.compAlongComposition p c is controlled by the product of the norms of the relevant bits of f and p.

          theorem FormalMultilinearSeries.compAlongComposition_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : } (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
          q.compAlongComposition p c q c.length * i : Fin c.length, p (c.blocksFun i)

          The norm of q.compAlongComposition p c is controlled by the product of the norms of the relevant bits of q and p.

          theorem FormalMultilinearSeries.compAlongComposition_nnnorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : } (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n) :
          q.compAlongComposition p c‖₊ q c.length‖₊ * i : Fin c.length, p (c.blocksFun i)‖₊

          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. We allow an arbitrary constant coefficient x.

          Equations
          Instances For
            @[simp]
            theorem FormalMultilinearSeries.id_apply_zero (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (v : Fin 0E) :
            (FormalMultilinearSeries.id 𝕜 E x 0) v = x
            @[simp]
            theorem FormalMultilinearSeries.id_apply_one (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (v : Fin 1E) :
            (FormalMultilinearSeries.id 𝕜 E x 1) v = v 0

            The first coefficient of id 𝕜 E is the identity.

            theorem FormalMultilinearSeries.id_apply_one' (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) {n : } (h : n = 1) (v : Fin nE) :
            (FormalMultilinearSeries.id 𝕜 E x n) v = v 0,

            The nth 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.

            @[simp]
            theorem FormalMultilinearSeries.id_apply_of_one_lt (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) {n : } (h : 1 < n) :

            For n ≠ 1, the n-th coefficient of id 𝕜 E is zero, by definition.

            @[simp]
            theorem FormalMultilinearSeries.comp_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : E) :
            p.comp (FormalMultilinearSeries.id 𝕜 E x) = p
            @[simp]
            theorem FormalMultilinearSeries.id_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (v0 : Fin 0E) :
            (FormalMultilinearSeries.id 𝕜 F ((p 0) v0)).comp p = p
            theorem FormalMultilinearSeries.id_comp' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (x : F) (v0 : Fin 0E) (h : x = (p 0) v0) :
            (FormalMultilinearSeries.id 𝕜 F x).comp p = p

            Variant of id_comp in which the zero coefficient is given by an equality hypothesis instead of a definitional equality. Useful for rewriting or simplifying out in some situations.

            Summability properties of the composition of formal power series #

            theorem FormalMultilinearSeries.comp_summable_nnreal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (hq : 0 < q.radius) (hp : 0 < p.radius) :
            r > 0, Summable fun (i : (n : ) × Composition n) => q.compAlongComposition p i.snd‖₊ * r ^ i.fst

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

            theorem FormalMultilinearSeries.le_comp_radius_of_summable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (r : NNReal) (hr : Summable fun (i : (n : ) × Composition n) => q.compAlongComposition p i.snd‖₊ * r ^ i.fst) :
            r (q.comp p).radius

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

            def FormalMultilinearSeries.compPartialSumSource (m : ) (M : ) (N : ) :
            Finset ((n : ) × (Fin n))

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

            Equations
            Instances For
              @[simp]
              theorem FormalMultilinearSeries.mem_compPartialSumSource_iff (m : ) (M : ) (N : ) (i : (n : ) × (Fin n)) :
              i FormalMultilinearSeries.compPartialSumSource m M N (m i.fst i.fst < M) ∀ (a : Fin i.fst), 1 i.snd a i.snd a < N

              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
                @[simp]
                theorem FormalMultilinearSeries.compChangeOfVariables_blocksFun (m : ) (M : ) (N : ) {i : (n : ) × (Fin n)} (hi : i FormalMultilinearSeries.compPartialSumSource m M N) (j : Fin i.fst) :
                (FormalMultilinearSeries.compChangeOfVariables m M N i hi).snd.blocksFun j, = i.snd j

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

                Equations
                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_partialSum.

                  Equations
                  Instances For
                    @[simp]
                    theorem FormalMultilinearSeries.mem_compPartialSumTarget_iff {m : } {M : } {N : } {a : (n : ) × Composition n} :
                    a FormalMultilinearSeries.compPartialSumTarget m M N m a.snd.length a.snd.length < M ∀ (j : Fin a.snd.length), a.snd.blocksFun j < N
                    theorem FormalMultilinearSeries.compChangeOfVariables_sum {α : Type u_6} [AddCommMonoid α] (m : ) (M : ) (N : ) (f : (n : ) × (Fin n)α) (g : (n : ) × Composition nα) (h : ∀ (e : (n : ) × (Fin n)) (he : e FormalMultilinearSeries.compPartialSumSource m M N), f e = g (FormalMultilinearSeries.compChangeOfVariables m M N e he)) :

                    compChangeOfVariables m M N is a bijection between compPartialSumSource m M N and compPartialSumTarget m M N, yielding equal sums for functions that correspond to each other under the bijection. As compChangeOfVariables 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.

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

                    theorem FormalMultilinearSeries.comp_partialSum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (M : ) (N : ) (z : E) :
                    q.partialSum M (∑ iFinset.Ico 1 N, (p i) fun (_j : Fin i) => z) = iFormalMultilinearSeries.compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun (_j : Fin i.fst) => z

                    Composing the partial sums of two multilinear series coincides with the sum over all compositions in compPartialSumTarget 0 N N. This is precisely the motivation for the definition of compPartialSumTarget.

                    theorem HasFPowerSeriesWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {t : Set F} {s : Set E} (hg : HasFPowerSeriesWithinAt g q t (f x)) (hf : HasFPowerSeriesWithinAt f p s x) (hs : Set.MapsTo f s t) :
                    HasFPowerSeriesWithinAt (g f) (q.comp p) s x

                    If two functions g and f have power series q and p respectively at f x and x, within two sets s and t such that f maps s to t, then g ∘ f admits the power series q.comp p at x within s.

                    theorem HasFPowerSeriesAt.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E} (hg : HasFPowerSeriesAt g q (f x)) (hf : HasFPowerSeriesAt f p x) :
                    HasFPowerSeriesAt (g f) (q.comp p) x

                    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 within s.

                    theorem AnalyticWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {x : E} {t : Set F} {s : Set E} (hg : AnalyticWithinAt 𝕜 g t (f x)) (hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t) :
                    AnalyticWithinAt 𝕜 (g f) s x

                    If two functions g and f are analytic respectively at f x and x, within two sets s and t such that f maps s to t, then g ∘ f is analytic at x within s.

                    theorem AnalyticWithinAt.comp_of_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {y : F} {x : E} {t : Set F} {s : Set E} (hg : AnalyticWithinAt 𝕜 g t y) (hf : AnalyticWithinAt 𝕜 f s x) (h : Set.MapsTo f s t) (hy : f x = y) :
                    AnalyticWithinAt 𝕜 (g f) s x

                    Version of AnalyticWithinAt.comp where point equality is a separate hypothesis.

                    theorem AnalyticOn.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : FG} {g : EF} {s : Set F} {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
                    AnalyticOn 𝕜 (f g) t
                    @[deprecated AnalyticOn.comp]
                    theorem AnalyticWithinOn.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : FG} {g : EF} {s : Set F} {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
                    AnalyticOn 𝕜 (f g) t

                    Alias of AnalyticOn.comp.

                    theorem AnalyticAt.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {x : E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) :
                    AnalyticAt 𝕜 (g f) x

                    If two functions g and f are analytic respectively at f x and x, then g ∘ f is analytic at x.

                    theorem AnalyticAt.comp_of_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {y : F} {x : E} (hg : AnalyticAt 𝕜 g y) (hf : AnalyticAt 𝕜 f x) (hy : f x = y) :
                    AnalyticAt 𝕜 (g f) x

                    Version of AnalyticAt.comp where point equality is a separate hypothesis.

                    theorem AnalyticAt.comp_analyticWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {x : E} {s : Set E} (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticWithinAt 𝕜 f s x) :
                    AnalyticWithinAt 𝕜 (g f) s x
                    theorem AnalyticAt.comp_analyticWithinAt_of_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : FG} {f : EF} {x : E} {y : F} {s : Set E} (hg : AnalyticAt 𝕜 g y) (hf : AnalyticWithinAt 𝕜 f s x) (h : f x = y) :
                    AnalyticWithinAt 𝕜 (g f) s x
                    theorem AnalyticOnNhd.comp' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {g : FG} {f : EF} (hg : AnalyticOnNhd 𝕜 g (f '' s)) (hf : AnalyticOnNhd 𝕜 f s) :
                    AnalyticOnNhd 𝕜 (g f) s

                    If two functions g and f are analytic respectively on s.image f and s, then g ∘ f is analytic on s.

                    @[deprecated AnalyticOnNhd.comp']
                    theorem AnalyticOn.comp' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {g : FG} {f : EF} (hg : AnalyticOnNhd 𝕜 g (f '' s)) (hf : AnalyticOnNhd 𝕜 f s) :
                    AnalyticOnNhd 𝕜 (g f) s

                    Alias of AnalyticOnNhd.comp'.


                    If two functions g and f are analytic respectively on s.image f and s, then g ∘ f is analytic on s.

                    theorem AnalyticOnNhd.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {t : Set F} {g : FG} {f : EF} (hg : AnalyticOnNhd 𝕜 g t) (hf : AnalyticOnNhd 𝕜 f s) (st : Set.MapsTo f s t) :
                    AnalyticOnNhd 𝕜 (g f) s
                    theorem AnalyticOnNhd.comp_analyticOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : FG} {g : EF} {s : Set F} {t : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
                    AnalyticOn 𝕜 (f g) t
                    @[deprecated AnalyticOnNhd.comp_analyticOn]
                    theorem AnalyticOn.comp_analyticWithinOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : FG} {g : EF} {s : Set F} {t : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) :
                    AnalyticOn 𝕜 (f g) t

                    Alias of AnalyticOnNhd.comp_analyticOn.

                    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.

                    theorem Composition.sigma_composition_eq_iff {n : } (i : (a : Composition n) × Composition a.length) (j : (a : Composition n) × Composition a.length) :
                    i = j i.fst.blocks = j.fst.blocks i.snd.blocks = j.snd.blocks

                    Rewriting equality in the dependent type Σ (a : Composition n), Composition a.length) in non-dependent terms with lists, requiring that the blocks coincide.

                    theorem Composition.sigma_pi_composition_eq_iff {n : } (u : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) (v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) :
                    u = v (List.ofFn fun (i : Fin u.fst.length) => (u.snd i).blocks) = List.ofFn fun (i : Fin v.fst.length) => (v.snd i).blocks

                    Rewriting equality in the dependent type Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun i) in non-dependent terms with lists, requiring that the lists of blocks coincide.

                    def Composition.gather {n : } (a : Composition n) (b : Composition a.length) :

                    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
                    • a.gather b = { blocks := List.map List.sum (a.blocks.splitWrtComposition b), blocks_pos := , blocks_sum := }
                    Instances For
                      theorem Composition.length_gather {n : } (a : Composition n) (b : Composition a.length) :
                      (a.gather b).length = b.length
                      def Composition.sigmaCompositionAux {n : } (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length) :
                      Composition ((a.gather b).blocksFun i)

                      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
                      • a.sigmaCompositionAux b i = { blocks := (a.blocks.splitWrtComposition b)[i], blocks_pos := , blocks_sum := }
                      Instances For
                        theorem Composition.length_sigmaCompositionAux {n : } (a : Composition n) (b : Composition a.length) (i : Fin b.length) :
                        (a.sigmaCompositionAux b i, ).length = b.blocksFun i
                        theorem Composition.blocksFun_sigmaCompositionAux {n : } (a : Composition n) (b : Composition a.length) (i : Fin b.length) (j : Fin (b.blocksFun i)) :
                        (a.sigmaCompositionAux b i, ).blocksFun j, = a.blocksFun ((b.embedding i) j)
                        theorem Composition.sizeUpTo_sizeUpTo_add {n : } (a : Composition n) (b : Composition a.length) {i : } {j : } (hi : i < b.length) (hj : j < b.blocksFun i, hi) :
                        a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b i, ).sizeUpTo j

                        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 sizeUpTo 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 sigmaCompositionAux a b. This is the content of this lemma.

                        def Composition.sigmaEquivSigmaPi (n : ) :
                        (a : Composition n) × Composition a.length (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))

                        Natural equivalence between (Σ (a : Composition n), Composition a.length) and (Σ (c : Composition n), Π (i : Fin c.length), Composition (c.blocksFun 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.
                        Instances For
                          theorem FormalMultilinearSeries.comp_assoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] (r : FormalMultilinearSeries 𝕜 G H) (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
                          (r.comp q).comp p = r.comp (q.comp p)