Mathlib.Analysis.Analytic.Inverse

Module docstring

{"# Inverse of analytic functions

We construct the left and right inverse of a formal multilinear series with invertible linear term, we prove that they coincide and study their properties (notably convergence). We deduce that the inverse of an analytic partial homeomorphism is analytic.

Main statements

p.leftInv i x: the formal left inverse of the formal multilinear series p, with constant coefficient x, for i : E ≃L[𝕜] F which coincides with p₁.
p.rightInv i x: the formal right inverse of the formal multilinear series p, with constant coefficient x, for i : E ≃L[𝕜] F which coincides with p₁.
p.leftInv_comp says that p.leftInv i x is indeed a left inverse to p when p₁ = i.
p.rightInv_comp says that p.rightInv i x is indeed a right inverse to p when p₁ = i.
p.leftInv_eq_rightInv: the two inverses coincide.
p.radius_rightInv_pos_of_radius_pos: if a power series has a positive radius of convergence, then so does its inverse.
PartialHomeomorph.hasFPowerSeriesAt_symm shows that, if a partial homeomorph has a power series p at a point, with invertible linear part, then the inverse also has a power series at the image point, given by p.leftInv. ","### The left inverse of a formal multilinear series ","### The right inverse of a formal multilinear series ","### Coincidence of the left and the right inverse ","### Convergence of the inverse of a power series

Assume that p is a convergent multilinear series, and let q be its (left or right) inverse. Using the left-inverse formula gives $$ qn = - (p1)^{-n} \sum{k=0}^{n-1} \sum{i1 + \dotsc + ik = n} qk (p{i1}, \dotsc, p{i_k}). $$ Assume for simplicity that we are in dimension 1 and p₁ = 1. In the formula for qₙ, the term q_{n-1} appears with a multiplicity of n-1 (choosing the index i_j for which i_j = 2 while all the other indices are equal to 1), which indicates that qₙ might grow like n!. This is bad for summability properties.

It turns out that the right-inverse formula is better behaved, and should instead be used for this kind of estimate. It reads $$ qn = - (p1)^{-1} \sum{k=2}^n \sum{i1 + \dotsc + ik = n} pk (q{i1}, \dotsc, q{i_k}). $$ Here, q_{n-1} can only appear in the term with k = 2, and it only appears twice, so there is hope this formula can lead to an at most geometric behavior.

Let Qₙ = ‖qₙ‖. Bounding ‖pₖ‖ with C r^k gives an inequality $$ Qn ≤ C' \sum{k=2}^n r^k \sum{i1 + \dotsc + ik = n} Q{i1} \dotsm Q{i_k}. $$

This formula is not enough to prove by naive induction on n a bound of the form Qₙ ≤ D R^n. However, assuming that the inequality above were an equality, one could get a formula for the generating series of the Qₙ:

$$ \begin{align} Q(z) & := \sum Qn z^n = Q1 z + C' \sum{2 \leq k \leq n} \sum{i1 + \dotsc + ik = n} (r z^{i1} Q{i1}) \dotsm (r z^{ik} Q{ik}) \\ & = Q1 z + C' \sum{k = 2}^\infty (\sum{i1 \geq 1} r z^{i1} Q{i1}) \dotsm (\sum{ik \geq 1} r z^{ik} Q{ik}) \\ & = Q1 z + C' \sum{k = 2}^\infty (r Q(z))^k = Q_1 z + C' (r Q(z))^2 / (1 - r Q(z)). \end{align} $$

One can solve this formula explicitly. The solution is analytic in a neighborhood of 0 in ℂ, hence its coefficients grow at most geometrically (by a contour integral argument), and therefore the original Qₙ, which are bounded by these ones, are also at most geometric.

This classical argument is not really satisfactory, as it requires an a priori bound on a complex analytic function. Another option would be to compute explicitly its terms (with binomial coefficients) to obtain an explicit geometric bound, but this would be very painful.

Instead, we will use the above intuition, but in a slightly different form, with finite sums and an induction. I learnt this trick in [poeschel2017siegelsternberg]. Let $Sn = \sum{k=1}^n Q_k a^k$ (where a is a positive real parameter to be chosen suitably small). The above computation but with finite sums shows that

$$ Sn \leq Q1 a + C' \sum{k=2}^n (r S{n-1})^k. $$

In particular, $Sn \leq Q1 a + C' (r S{n-1})^2 / (1- r S{n-1})$. Assume that $S{n-1} \leq K a$, where K > Q₁ is fixed and a is small enough so that r K a ≤ 1/2 (to control the denominator). Then this equation gives a bound $Sn \leq Q_1 a + 2 C' r^2 K^2 a^2$. If a is small enough, this is bounded by K a as the second term is quadratic in a, and therefore negligible.

By induction, we deduce Sₙ ≤ K a for all n, which gives in particular the fact that aⁿ Qₙ remains bounded. ","### The inverse of an analytic partial homeomorphism is analytic "}

FormalMultilinearSeries.leftInv definition

(p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 F E

Full source

/-- The left inverse of a formal multilinear series, where the `n`-th term is defined inductively
in terms of the previous ones to make sure that `(leftInv p i) ∘ p = id`. For this, the linear term
`p₁` in `p` should be invertible. In the definition, `i` is a linear isomorphism that should
coincide with `p₁`, so that one can use its inverse in the construction. The definition does not
use that `i = p₁`, but proofs that the definition is well-behaved do.

The `n`-th term in `q ∘ p` is `∑ qₖ (p_{j₁}, ..., p_{jₖ})` over `j₁ + ... + jₖ = n`. In this
expression, `qₙ` appears only once, in `qₙ (p₁, ..., p₁)`. We adjust the definition so that this
term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`.

These formulas only make sense when the constant term `p₀` vanishes. The definition we give is
general, but it ignores the value of `p₀`.
-/
noncomputable def leftInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    FormalMultilinearSeries 𝕜 F E
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ x
  | 1 => (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm
  | n + 2 =>
    -∑ c : { c : Composition (n + 2) // c.length < n + 2 },
        (leftInv p i x (c : Composition (n + 2)).length).compAlongComposition
          (p.compContinuousLinearMap i.symm) c

Left inverse of a formal multilinear series

Informal description

The left inverse of a formal multilinear series $p$ from $E$ to $F$ with respect to a continuous linear equivalence $i : E \simeq F$ and a constant term $x \in E$ is a formal multilinear series from $F$ to $E$ defined inductively as follows: - The zeroth term is the constant multilinear map with value $x$. - The first term is the inverse of $i$. - For $n + 2$, the term is constructed as the negative sum over all compositions $c$ of $n + 2$ with length less than $n + 2$ of the composition of the $(c.\text{length})$-th term of the left inverse with the series $p$ precomposed with $i^{-1}$ along the composition $c$. This construction ensures that the composition of the left inverse with $p$ yields the identity series, provided that the linear term $p_1$ coincides with $i$.

FormalMultilinearSeries.leftInv_coeff_zero theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x

Full source

@[simp]
theorem leftInv_coeff_zero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x := by rw [leftInv]

Zeroth coefficient of left inverse equals constant map

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, $i : E \simeq F$ a continuous linear equivalence, and $x \in E$. Then the zeroth coefficient of the left inverse series $p.\text{leftInv}\,i\,x$ equals the constant multilinear map with value $x$.

FormalMultilinearSeries.leftInv_coeff_one theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
  p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm

Full source

@[simp]
theorem leftInv_coeff_one (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm := by rw [leftInv]

First Coefficient of Left Inverse Equals Inverse Linear Term

Informal description

For any formal multilinear series $p$ from $E$ to $F$, continuous linear equivalence $i : E \simeq F$, and constant term $x \in E$, the first coefficient of the left inverse series $p.\text{leftInv}\,i\,x$ is equal to the inverse of $i$, when viewed as a continuous linear map via the canonical isomorphism between linear maps and 1-multilinear maps.

FormalMultilinearSeries.leftInv_removeZero theorem

(p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.leftInv i x = p.leftInv i x

Full source

/-- The left inverse does not depend on the zeroth coefficient of a formal multilinear
series. -/
theorem leftInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.removeZero.leftInv i x = p.leftInv i x := by
  ext1 n
  induction' n using Nat.strongRec' with n IH
  match n with
  | 0 => simp -- if one replaces `simp` with `refl`, the proof times out in the kernel.
  | 1 => simp -- TODO: why?
  | n + 2 =>
    simp only [leftInv, neg_inj]
    refine Finset.sum_congr rfl fun c cuniv => ?_
    rcases c with ⟨c, hc⟩
    ext v
    dsimp
    simp [IH _ hc]

Left Inverse is Unaffected by Removal of Zeroth Coefficient

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, $i : E \simeq F$ a continuous linear equivalence, and $x \in E$. Then the left inverse of the series $p.\text{removeZero}$ with respect to $i$ and $x$ is equal to the left inverse of the original series $p$ with respect to $i$ and $x$. In other words, removing the zeroth coefficient from $p$ does not affect its left inverse construction: \[ (p.\text{removeZero}).\text{leftInv}\,i\,x = p.\text{leftInv}\,i\,x. \]

FormalMultilinearSeries.leftInv_comp theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
  (leftInv p i x).comp p = id 𝕜 E x

Full source

/-- The left inverse to a formal multilinear series is indeed a left inverse, provided its linear
term is invertible. -/
theorem leftInv_comp (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    (leftInv p i x).comp p = id 𝕜 E x := by
  ext n v
  classical
  match n with
  | 0 =>
    simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply,
      id_apply_zero]
  | 1 =>
    simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply,
      ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have A :
      (Finset.univ : Finset (Composition (n + 2))) =
        {c | Composition.length c < n + 2}{c | Composition.length c < n + 2}.toFinset ∪ {Composition.ones (n + 2)} := by
      refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
      by_cases h : c.length < n + 2
      · simp [h, Set.mem_toFinset (s := {c | Composition.length c < n + 2})]
      · simp [Composition.eq_ones_iff_le_length.2 (not_lt.1 h)]
    have B :
      Disjoint ({c | Composition.length c < n + 2} : Set (Composition (n + 2))).toFinset
        {Composition.ones (n + 2)} := by
      simp [Set.mem_toFinset (s := {c | Composition.length c < n + 2})]
    have C :
      ((p.leftInv i x (Composition.ones (n + 2)).length)
          fun j : Fin (Composition.ones n.succ.succ).length =>
          p 1 fun _ => v ((Fin.castLE (Composition.length_le _)) j)) =
        p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by
      apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_
      exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr
    have D :
      (p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j) =
        -∑ c ∈ {c : Composition (n + 2) | c.length < n + 2}.toFinset,
            (p.leftInv i x c.length) (p.applyComposition c v) := by
      simp only [leftInv, ContinuousMultilinearMap.neg_apply, neg_inj,
        ContinuousMultilinearMap.sum_apply]
      convert
        (sum_toFinset_eq_subtype
          (fun c : Composition (n + 2) => c.length < n + 2)
          (fun c : Composition (n + 2) =>
          (ContinuousMultilinearMap.compAlongComposition
            (p.compContinuousLinearMap (i.symm : F →L[𝕜] E)) c (p.leftInv i x c.length))
            fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans
          _
      simp only [compContinuousLinearMap_applyComposition,
        ContinuousMultilinearMap.compAlongComposition_apply]
      congr
      ext c
      congr
      ext k
      simp [h, Function.comp_def]
    simp [FormalMultilinearSeries.comp, show n + 2 ≠ 1 by omega, A, Finset.sum_union B,
      applyComposition_ones, C, D, -Set.toFinset_setOf]

Left Inverse Property for Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, and let $i : E \simeq F$ be a continuous linear equivalence such that the linear term $p_1$ of $p$ coincides with $i$ (i.e., $p_1 = i$ when viewed as a 1-multilinear map). Then the composition of the left inverse series $p.\text{leftInv}\,i\,x$ with $p$ equals the identity formal multilinear series $\text{id}_{\mathbb{K}, E}(x)$, where $x \in E$ is the constant term. In other words, under the given assumptions: $$(p.\text{leftInv}\,i\,x) \circ p = \text{id}_{\mathbb{K}, E}(x).$$

FormalMultilinearSeries.rightInv definition

(p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 F E

Full source

/-- The right inverse of a formal multilinear series, where the `n`-th term is defined inductively
in terms of the previous ones to make sure that `p ∘ (rightInv p i) = id`. For this, the linear
term `p₁` in `p` should be invertible. In the definition, `i` is a linear isomorphism that should
coincide with `p₁`, so that one can use its inverse in the construction. The definition does not
use that `i = p₁`, but proofs that the definition is well-behaved do.

The `n`-th term in `p ∘ q` is `∑ pₖ (q_{j₁}, ..., q_{jₖ})` over `j₁ + ... + jₖ = n`. In this
expression, `qₙ` appears only once, in `p₁ (qₙ)`. We adjust the definition of `qₙ` so that this
term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`.

These formulas only make sense when the constant term `p₀` vanishes. The definition we give is
general, but it ignores the value of `p₀`.
-/
noncomputable def rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    FormalMultilinearSeries 𝕜 F E
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ x
  | 1 => (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm
  | n + 2 =>
    let q : FormalMultilinearSeries 𝕜 F E := fun k => if k < n + 2 then rightInv p i x k else 0;
    -(i.symm : F →L[𝕜] E).compContinuousMultilinearMap ((p.comp q) (n + 2))

Right inverse of a formal multilinear series

Informal description

The right inverse of a formal multilinear series $ p $ from $ E $ to $ F $ over a field $ \mathbb{K} $, given a linear isomorphism $ i : E \simeq F $ and a base point $ x \in E $, is a formal multilinear series $ q $ from $ F $ to $ E $ defined inductively as follows: - The zeroth coefficient $ q_0 $ is the constant multilinear map with value $ x $. - The first coefficient $ q_1 $ is the inverse of $ i $, interpreted as a linear map from $ F $ to $ E $. - For $ n + 2 $, the coefficient $ q_{n+2} $ is defined recursively to ensure that the composition $ p \circ q $ is the identity series. Specifically, it is given by \[ q_{n+2} = -i^{-1} \circ \left( p \circ q \right)_{n+2}, \] where $ \left( p \circ q \right)_{n+2} $ is the $(n+2)$-th coefficient of the composition of $ p $ and $ q $, and $ i^{-1} $ is the inverse of the linear isomorphism $ i $. This construction ensures that $ p \circ q $ behaves like the identity series, modulo the constant term $ p_0 $, which is ignored in the definition.

FormalMultilinearSeries.rightInv_coeff_zero theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
  p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x

Full source

@[simp]
theorem rightInv_coeff_zero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ x := by rw [rightInv]

Zeroth Coefficient of Right Inverse Formal Multilinear Series

Informal description

For any formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, given a linear isomorphism $i : E \simeq F$ and a base point $x \in E$, the zeroth coefficient of the right inverse series $q = p.\text{rightInv}\ i\ x$ is the constant multilinear map with value $x$. That is, $q_0 = x$.

FormalMultilinearSeries.rightInv_coeff_one theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
  p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm

Full source

@[simp]
theorem rightInv_coeff_one (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm := by rw [rightInv]

First Coefficient of Right Inverse Equals Inverse Linear Isomorphism

Informal description

For any formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, any linear isomorphism $i : E \simeq F$, and any base point $x \in E$, the first coefficient of the right inverse series $q = p.\text{rightInv}\ i\ x$ is equal to the inverse of $i$, interpreted as a continuous linear map from $F$ to $E$. More precisely, we have: \[ q_1 = i^{-1} \] where $q_1$ is the first coefficient of the right inverse series, and $i^{-1}$ is the inverse of the linear isomorphism $i$.

FormalMultilinearSeries.rightInv_removeZero theorem

(p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.rightInv i x = p.rightInv i x

Full source

/-- The right inverse does not depend on the zeroth coefficient of a formal multilinear
series. -/
theorem rightInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.removeZero.rightInv i x = p.rightInv i x := by
  ext1 n
  induction' n using Nat.strongRec' with n IH
  match n with
  | 0 => simp only [rightInv_coeff_zero]
  | 1 => simp only [rightInv_coeff_one]
  | n + 2 =>
    simp only [rightInv, neg_inj]
    rw [removeZero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
    congr (config := { closePost := false }) 2 with k
    by_cases hk : k < n + 2 <;> simp [hk, IH]

Right Inverse Unaffected by Removal of Zeroth Term: $p.\text{removeZero}^{-1} = p^{-1}$

Informal description

For any formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, any linear isomorphism $i : E \simeq F$, and any base point $x \in E$, the right inverse of the series $p.\text{removeZero}$ (where the zeroth coefficient is set to zero) is equal to the right inverse of the original series $p$. In other words, removing the zeroth coefficient from $p$ does not affect its right inverse construction.

FormalMultilinearSeries.comp_rightInv_aux1 theorem

 {n : ℕ} (hn : 0 < n) (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 F E) (v : Fin n → F) :
  p.comp q n v =
    ∑ c ∈ {c : Composition n | 1 < c.length}.toFinset, p c.length (q.applyComposition c v) + p 1 fun _ => q n v

Full source

theorem comp_rightInv_aux1 {n : ℕ} (hn : 0 < n) (p : FormalMultilinearSeries 𝕜 E F)
    (q : FormalMultilinearSeries 𝕜 F E) (v : Fin n → F) :
    p.comp q n v =
      ∑ c ∈ {c : Composition n | 1 < c.length}.toFinset,
          p c.length (q.applyComposition c v) + p 1 fun _ => q n v := by
  classical
  have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}{c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h, Set.mem_toFinset (s := {c | 1 < Composition.length c})]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]
  have B :
    Disjoint ({c | 1 < Composition.length c} : Set (Composition n)).toFinset
      {Composition.single n hn} := by
    simp [Set.mem_toFinset (s := {c | 1 < Composition.length c})]
  have C :
    p (Composition.single n hn).length (q.applyComposition (Composition.single n hn) v) =
      p 1 fun _ : Fin 1 => q n v := by
    apply p.congr (Composition.single_length hn) fun j hj1 _ => ?_
    simp [applyComposition_single]
  simp [FormalMultilinearSeries.comp, A, Finset.sum_union B, C, -Set.toFinset_setOf,
    -add_right_inj, -Composition.single_length]

Decomposition of Composition of Formal Multilinear Series for Positive Degree

Informal description

For any positive integer $n$, formal multilinear series $p$ from $E$ to $F$ and $q$ from $F$ to $E$ over a field $\mathbb{K}$, and any vector-valued function $v : \text{Fin } n \to F$, the $n$-th coefficient of the composition $p \circ q$ evaluated at $v$ can be expressed as: \[ (p \circ q)_n(v) = \sum_{\substack{c \text{ composition of } n \\ \text{length}(c) > 1}} p_{\text{length}(c)}(q.\text{applyComposition}_c(v)) + p_1(\lambda \_. q_n(v)) \] where the first sum is over all compositions $c$ of $n$ with length greater than 1, and the second term applies $p_1$ to the constant function returning $q_n(v)$.

FormalMultilinearSeries.comp_rightInv_aux2 theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (v : Fin (n + 2) → F) :
  ∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset,
      p c.length (applyComposition (fun k : ℕ => ite (k < n + 2) (p.rightInv i x k) 0) c v) =
    ∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset, p c.length ((p.rightInv i x).applyComposition c v)

Full source

theorem comp_rightInv_aux2 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ)
    (v : Fin (n + 2) → F) :
    ∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset,
        p c.length (applyComposition (fun k : ℕ => ite (k < n + 2) (p.rightInv i x k) 0) c v) =
      ∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset,
        p c.length ((p.rightInv i x).applyComposition c v) := by
  have N : 0 < n + 2 := by norm_num
  refine sum_congr rfl fun c hc => p.congr rfl fun j hj1 hj2 => ?_
  have : ∀ k, c.blocksFun k < n + 2 := by
    simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}),
      Set.mem_setOf_eq] at hc
    simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt hc]
  simp [applyComposition, this]

Equality of Sums in Right Inverse Composition for Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, $i : E \simeq F$ a linear isomorphism, $x \in E$, and $n \in \mathbb{N}$. For any $v : \text{Fin } (n+2) \to F$, the following sums are equal: \[ \sum_{\substack{c \text{ composition of } n+2 \\ \text{length}(c) > 1}} p_{\text{length}(c)}\left(\text{applyComposition} \left(\lambda k, \text{ite } (k < n+2) (q_k) 0\right) c \ v\right) = \sum_{\substack{c \text{ composition of } n+2 \\ \text{length}(c) > 1}} p_{\text{length}(c)}(q.\text{applyComposition}_c(v)) \] where $q = p.\text{rightInv} \ i \ x$ is the right inverse series of $p$.

FormalMultilinearSeries.comp_rightInv theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
  p.comp (rightInv p i x) = id 𝕜 F (p 0 0)

Full source

/-- The right inverse to a formal multilinear series is indeed a right inverse, provided its linear
term is invertible and its constant term vanishes. -/
theorem comp_rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    p.comp (rightInv p i x) = id 𝕜 F (p 0 0) := by
  ext (n v)
  match n with
  | 0 =>
    simp only [comp_coeff_zero', Matrix.zero_empty, id_apply_zero]
    congr
    ext i
    exact i.elim0
  | 1 =>
    simp only [comp_coeff_one, h, rightInv_coeff_one, ContinuousLinearEquiv.apply_symm_apply,
      id_apply_one, ContinuousLinearEquiv.coe_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have N : 0 < n + 2 := by norm_num
    simp [comp_rightInv_aux1 N, h, rightInv, lt_irrefl n, show n + 2 ≠ 1 by omega,
      ← sub_eq_add_neg, sub_eq_zero, comp_rightInv_aux2, -Set.toFinset_setOf]

Right Inverse Property for Formal Multilinear Series: $p \circ q = \text{id}$

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, and let $i : E \simeq F$ be a linear isomorphism such that the first coefficient $p_1$ of $p$ equals the linear isomorphism $i$ (interpreted as a multilinear map). Then the composition of $p$ with its right inverse series $q = p.\text{rightInv}\ i\ x$ is equal to the identity formal multilinear series on $F$ with constant term $p_0(0)$. In symbols: \[ p \circ q = \text{id}_{\mathbb{K}, F}(p_0(0)) \] where $\text{id}_{\mathbb{K}, F}(p_0(0))$ denotes the identity series with zeroth coefficient $p_0(0)$ and first coefficient the identity map on $F$.

FormalMultilinearSeries.rightInv_coeff theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (hn : 2 ≤ n) :
  p.rightInv i x n =
    -(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
        (∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition n)),
          p.compAlongComposition (p.rightInv i x) c)

Full source

theorem rightInv_coeff (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (n : ℕ) (hn : 2 ≤ n) :
    p.rightInv i x n =
      -(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
          (∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition n)),
            p.compAlongComposition (p.rightInv i x) c) := by
  match n with
  | 0 => exact False.elim (zero_lt_two.not_le hn)
  | 1 => exact False.elim (one_lt_two.not_le hn)
  | n + 2 =>
    simp only [rightInv, neg_inj]
    congr (config := { closePost := false }) 1
    ext v
    have N : 0 < n + 2 := by norm_num
    have : ((p 1) fun _ : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
    simp [comp_rightInv_aux1 N, lt_irrefl n, this, comp_rightInv_aux2, -Set.toFinset_setOf]

Coefficient Formula for Right Inverse of Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, $i : E \simeq F$ a linear isomorphism, and $x \in E$. For any natural number $n \geq 2$, the $n$-th coefficient of the right inverse series $q = p.\text{rightInv}\, i\, x$ is given by: \[ q_n = -i^{-1} \circ \left( \sum_{\substack{c \text{ composition of } n \\ \text{length}(c) > 1}} p.\text{compAlongComposition}\, q\, c \right) \] where the sum is over all compositions $c$ of $n$ with length greater than 1, and $i^{-1}$ is the inverse of the linear isomorphism $i$.

FormalMultilinearSeries.leftInv_eq_rightInv theorem

 (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
  leftInv p i x = rightInv p i x

Full source

theorem leftInv_eq_rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    leftInv p i x = rightInv p i x :=
  calc
    leftInv p i x = (leftInv p i x).comp (id 𝕜 F (p 0 0)) := by simp
    _ = (leftInv p i x).comp (p.comp (rightInv p i x)) := by rw [comp_rightInv p i _ h]
    _ = ((leftInv p i x).comp p).comp (rightInv p i x) := by rw [comp_assoc]
    _ = (id 𝕜 E x).comp (rightInv p i x) := by rw [leftInv_comp p i _ h]
    _ = rightInv p i x := by simp [id_comp' _ _ 0]

Equality of Left and Right Inverses for Formal Multilinear Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, and let $i : E \simeq F$ be a continuous linear isomorphism. Suppose the linear term $p_1$ of $p$ coincides with $i$ (when viewed as a 1-multilinear map). Then the left inverse series $p.\text{leftInv}\,i\,x$ and the right inverse series $p.\text{rightInv}\,i\,x$ are equal for any constant term $x \in E$. In other words, under the given assumptions: $$ p.\text{leftInv}\,i\,x = p.\text{rightInv}\,i\,x. $$

FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 theorem

 (n : ℕ) (p : ℕ → ℝ) (hp : ∀ k, 0 ≤ p k) {r a : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a) :
  ∑ k ∈ Ico 2 (n + 1),
      a ^ k *
        ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
          r ^ c.length * ∏ j, p (c.blocksFun j) ≤
    ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j

Full source

/-- First technical lemma to control the growth of coefficients of the inverse. Bound the explicit
expression for `∑_{k<n+1} aᵏ Qₖ` in terms of a sum of powers of the same sum one step before,
in a general abstract setup. -/
theorem radius_right_inv_pos_of_radius_pos_aux1 (n : ℕ) (p : ℕ → ℝ) (hp : ∀ k, 0 ≤ p k) {r a : ℝ}
    (hr : 0 ≤ r) (ha : 0 ≤ a) :
    ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
            r ^ c.length * ∏ j, p (c.blocksFun j) ≤
      ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j :=
  calc
    ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
              r ^ c.length * ∏ j, p (c.blocksFun j) =
        ∑ k ∈ Ico 2 (n + 1),
          ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
            ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j)) := by
      simp_rw [mul_sum]
      congr! with k _ c
      rw [prod_mul_distrib, prod_mul_distrib, prod_pow_eq_pow_sum, Composition.sum_blocksFun,
        prod_const, card_fin]
      ring
    _ ≤
        ∑ d ∈ compPartialSumTarget 2 (n + 1) n,
          ∏ j : Fin d.2.length, r * (a ^ d.2.blocksFun j * p (d.2.blocksFun j)) := by
      rw [sum_sigma']
      refine
        sum_le_sum_of_subset_of_nonneg ?_ fun x _ _ =>
          prod_nonneg fun j _ => mul_nonneg hr (mul_nonneg (pow_nonneg ha _) (hp _))
      rintro ⟨k, c⟩ hd
      simp only [Set.mem_toFinset (s := {c | 1 < Composition.length c}), mem_Ico, mem_sigma,
        Set.mem_setOf_eq] at hd
      simp only [mem_compPartialSumTarget_iff]
      refine ⟨hd.2, c.length_le.trans_lt hd.1.2, fun j => ?_⟩
      have : c ≠ Composition.single k (zero_lt_two.trans_le hd.1.1) := by
        simp [Composition.eq_single_iff_length, ne_of_gt hd.2]
      rw [Composition.ne_single_iff] at this
      exact (this j).trans_le (Nat.lt_succ_iff.mp hd.1.2)
    _ = ∑ e ∈ compPartialSumSource 2 (n + 1) n, ∏ j : Fin e.1, r * (a ^ e.2 j * p (e.2 j)) := by
      symm
      apply compChangeOfVariables_sum
      rintro ⟨k, blocksFun⟩ H
      have K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k := by simp
      congr 2 <;> try rw [K]
      rw [Fin.heq_fun_iff K.symm]
      intro j
      rw [compChangeOfVariables_blocksFun]
    _ = ∑ j ∈ Ico 2 (n + 1), r ^ j * (∑ k ∈ Ico 1 n, a ^ k * p k) ^ j := by
      rw [compPartialSumSource,
        ← sum_sigma' (Ico 2 (n + 1))
          (fun k : ℕ => (Fintype.piFinset fun _ : Fin k => Ico 1 n : Finset (Fin k → ℕ)))
          (fun n e => ∏ j : Fin n, r * (a ^ e j * p (e j)))]
      congr! with j
      simp only [← @MultilinearMap.mkPiAlgebra_apply ℝ (Fin j) _ ℝ]
      simp only [←
        MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) =>
          r * (a ^ m * p m)]
      simp only [MultilinearMap.mkPiAlgebra_apply]
      simp [prod_const, ← mul_sum, mul_pow]

Inequality for Sums of Compositions with Length Greater Than One: $\sum_{k=2}^{n+1} a^k \sum_{\text{length}(c) > 1} r^{\text{length}(c)} \prod_j p_{c_j} \leq \sum_{j=2}^{n+1} r^j (\sum_{k=1}^n a^k p_k)^j$

Informal description

For any natural number $n$, any nonnegative sequence $(p_k)_{k \in \mathbb{N}}$, and nonnegative real numbers $r$ and $a$, the following inequality holds: \[ \sum_{k=2}^{n+1} a^k \sum_{\substack{c \text{ composition of } k \\ \text{length}(c) > 1}} r^{\text{length}(c)} \prod_{j=1}^{\text{length}(c)} p_{c_j} \leq \sum_{j=2}^{n+1} r^j \left(\sum_{k=1}^n a^k p_k\right)^j. \] Here, the inner sum on the left is over all compositions $c$ of $k$ with length greater than 1, and $c_j$ denotes the size of the $j$-th block of the composition $c$.

FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2 theorem

 {x : E} {n : ℕ} (hn : 2 ≤ n + 1) (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) {r a C : ℝ} (hr : 0 ≤ r)
  (ha : 0 ≤ a) (hC : 0 ≤ C) (hp : ∀ n, ‖p n‖ ≤ C * r ^ n) :
  ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤
    ‖(i.symm : F →L[𝕜] E)‖ * a +
      ‖(i.symm : F →L[𝕜] E)‖ * C * ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k

Full source

/-- Second technical lemma to control the growth of coefficients of the inverse. Bound the explicit
expression for `∑_{k<n+1} aᵏ Qₖ` in terms of a sum of powers of the same sum one step before,
in the specific setup we are interesting in, by reducing to the general bound in
`radius_rightInv_pos_of_radius_pos_aux1`. -/
theorem radius_rightInv_pos_of_radius_pos_aux2 {x : E} {n : ℕ} (hn : 2 ≤ n + 1)
    (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) {r a C : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a)
    (hC : 0 ≤ C) (hp : ∀ n, ‖p n‖ ≤ C * r ^ n) :
    ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤
      ‖(i.symm : F →L[𝕜] E)‖ * a +
        ‖(i.symm : F →L[𝕜] E)‖ * C *
          ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k :=
  let I := ‖(i.symm : F →L[𝕜] E)‖
  calc
    ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ =
        a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖ := by
      simp only [I, LinearIsometryEquiv.norm_map, pow_one, rightInv_coeff_one,
        show Ico (1 : ℕ) 2 = {1} from Nat.Ico_succ_singleton 1,
        sum_singleton, ← sum_Ico_consecutive _ one_le_two hn]
    _ =
        a * I +
          ∑ k ∈ Ico 2 (n + 1),
            a ^ k *
              ‖(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
                  (∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
                    p.compAlongComposition (p.rightInv i x) c)‖ := by
      congr! 2 with j hj
      rw [rightInv_coeff _ _ _ _ (mem_Ico.1 hj).1, norm_neg]
    _ ≤
        a * ‖(i.symm : F →L[𝕜] E)‖ +
          ∑ k ∈ Ico 2 (n + 1),
            a ^ k *
              (I *
                ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
                  C * r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖) := by
      gcongr with j
      apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
      gcongr
      apply (norm_sum_le _ _).trans
      gcongr
      apply (compAlongComposition_norm _ _ _).trans
      gcongr
      apply hp
    _ = I * a + I * C * ∑ k ∈ Ico 2 (n + 1), a ^ k *
          ∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition k)),
            r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖ := by
      simp_rw [I, mul_assoc C, ← mul_sum, ← mul_assoc, mul_comm _ ‖(i.symm : F →L[𝕜] E)‖,
        mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum]
      ring
    _ ≤ I * a + I * C *
        ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k := by
      gcongr _ + _ * _ * ?_
      simp_rw [mul_pow]
      apply
        radius_right_inv_pos_of_radius_pos_aux1 n (fun k => ‖p.rightInv i x k‖)
          (fun k => norm_nonneg _) hr ha

Recursive Bound for Partial Sums of Right Inverse Coefficients: $\sum_{k=1}^{n+1} a^k \|q_k\| \leq \|i^{-1}\| a + \|i^{-1}\| C \sum_{k=2}^{n+1} (r \sum_{j=1}^n a^j \|q_j\|)^k$

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, $i : E \simeq F$ a linear isomorphism, and $x \in E$. Let $r, a, C \geq 0$ be real numbers such that $\|p_n\| \leq C r^n$ for all $n$. Then for any $n \geq 1$, the partial sum of weighted norms of the right inverse coefficients satisfies: \[ \sum_{k=1}^{n+1} a^k \|q_k\| \leq \|i^{-1}\| a + \|i^{-1}\| C \sum_{k=2}^{n+1} \left(r \sum_{j=1}^n a^j \|q_j\|\right)^k, \] where $q = p.\text{rightInv}\, i\, x$ is the right inverse series.

FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos theorem

{p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E} (hp : 0 < p.radius) : 0 < (p.rightInv i x).radius

Full source

/-- If a a formal multilinear series has a positive radius of convergence, then its right inverse
also has a positive radius of convergence. -/
theorem radius_rightInv_pos_of_radius_pos
    {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E}
    (hp : 0 < p.radius) : 0 < (p.rightInv i x).radius := by
  obtain ⟨C, r, Cpos, rpos, ple⟩ :
    ∃ (C r : _) (_ : 0 < C) (_ : 0 < r), ∀ n : ℕ, ‖p n‖ ≤ C * r ^ n :=
    le_mul_pow_of_radius_pos p hp
  let I := ‖(i.symm : F →L[𝕜] E)‖
  -- choose `a` small enough to make sure that `∑_{k ≤ n} aᵏ Qₖ` will be controllable by
  -- induction
  obtain ⟨a, apos, ha1, ha2⟩ :
    ∃ (a : _) (apos : 0 < a),
      2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1 ∧ r * (I + 1) * a ≤ 1 / 2 := by
    have :
      Tendsto (fun a => 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0)
        (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0)) :=
      tendsto_const_nhds.mul tendsto_id
    have A : ∀ᶠ a in 𝓝 0, 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a < 1 := by
      apply (tendsto_order.1 this).2; simp [zero_lt_one]
    have : Tendsto (fun a => r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0)) :=
      tendsto_const_nhds.mul tendsto_id
    have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1 / 2 := by
      apply (tendsto_order.1 this).2; simp [zero_lt_one]
    have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a := by
      filter_upwards [self_mem_nhdsWithin] with _ ha using ha
    rcases (C.and ((A.and B).filter_mono inf_le_left)).exists with ⟨a, ha⟩
    exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩
  -- check by induction that the partial sums are suitably bounded, using the choice of `a` and the
  -- inductive control from Lemma `radius_rightInv_pos_of_radius_pos_aux2`.
  let S n := ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
  have IRec : ∀ n, 1 ≤ n → S n ≤ (I + 1) * a := by
    apply Nat.le_induction
    · simp only [S]
      rw [Ico_eq_empty_of_le (le_refl 1), sum_empty]
      exact mul_nonneg (add_nonneg (norm_nonneg _) zero_le_one) apos.le
    · intro n one_le_n hn
      have In : 2 ≤ n + 1 := by omega
      have rSn : r * S n ≤ 1 / 2 :=
        calc
          r * S n ≤ r * ((I + 1) * a) := by gcongr
          _ ≤ 1 / 2 := by rwa [← mul_assoc]
      calc
        S (n + 1) ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k :=
          radius_rightInv_pos_of_radius_pos_aux2 In p i rpos.le apos.le Cpos.le ple
        _ = I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) := by
          rw [geom_sum_Ico' _ In]; exact ne_of_lt (rSn.trans_lt (by norm_num))
        _ ≤ I * a + I * C * ((r * S n) ^ 2 / (1 / 2)) := by
          gcongr
          · simp only [sub_le_self_iff]
            positivity
          · linarith only [rSn]
        _ = I * a + 2 * I * C * (r * S n) ^ 2 := by ring
        _ ≤ I * a + 2 * I * C * (r * ((I + 1) * a)) ^ 2 := by gcongr
        _ = (I + 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) * a := by ring
        _ ≤ (I + 1) * a := by gcongr
  -- conclude that all coefficients satisfy `aⁿ Qₙ ≤ (I + 1) a`.
  let a' : NNReal := ⟨a, apos.le⟩
  suffices H : (a' : ENNReal) ≤ (p.rightInv i x).radius by
    apply lt_of_lt_of_le _ H
    -- Prior to https://github.com/leanprover/lean4/pull/2734, this was `exact_mod_cast apos`.
    simpa only [ENNReal.coe_pos]
  apply le_radius_of_eventually_le _ ((I + 1) * a)
  filter_upwards [Ici_mem_atTop 1] with n (hn : 1 ≤ n)
  calc
    ‖p.rightInv i x n‖ * (a' : ℝ) ^ n = a ^ n * ‖p.rightInv i x n‖ := mul_comm _ _
    _ ≤ ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ :=
      (haveI : ∀ k ∈ Ico 1 (n + 1), 0 ≤ a ^ k * ‖p.rightInv i x k‖ := fun k _ => by positivity
      single_le_sum this (by simp [hn]))
    _ ≤ (I + 1) * a := IRec (n + 1) (by norm_num)

Positivity of the Radius of Convergence for the Right Inverse of a Formal Power Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, with a positive radius of convergence. Given a linear isomorphism $i : E \simeq F$ and a base point $x \in E$, the right inverse series $q = p.\text{rightInv}\, i\, x$ also has a positive radius of convergence.

FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos theorem

 {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E} (hp : 0 < p.radius)
  (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) : 0 < (p.leftInv i x).radius

Full source

/-- If a a formal multilinear series has a positive radius of convergence, then its left inverse
also has a positive radius of convergence. -/
theorem radius_leftInv_pos_of_radius_pos
    {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E}
    (hp : 0 < p.radius) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    0 < (p.leftInv i x).radius := by
  rw [leftInv_eq_rightInv _ _ _ h]
  exact radius_rightInv_pos_of_radius_pos hp

Positivity of the Radius of Convergence for the Left Inverse of a Formal Power Series

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$ with positive radius of convergence. Given a continuous linear isomorphism $i : E \simeq F$ and a point $x \in E$, if the linear term $p_1$ of $p$ coincides with $i$ (when viewed as a 1-multilinear map), then the left inverse series $p.\text{leftInv}\,i\,x$ also has a positive radius of convergence.

HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp theorem

 {f : E → G} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
  (hf : HasFPowerSeriesAt f (q.comp p) x) (hq : 0 < q.radius) (hp : 0 < p.radius) :
  ∀ᶠ y in 𝓝 0, Tendsto (fun (a : ℕ × ℕ) ↦ q.partialSum a.1 (p.partialSum a.2 y - p 0 (fun _ ↦ 0))) atTop (𝓝 (f (x + y)))

Full source

lemma HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp
    {f : E → G} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hf : HasFPowerSeriesAt f (q.comp p) x) (hq : 0 < q.radius) (hp : 0 < p.radius) :
    ∀ᶠ y in 𝓝 0, Tendsto (fun (a : ℕ × ℕ) ↦ q.partialSum a.1 (p.partialSum a.2 y
      - p 0 (fun _ ↦ 0))) atTop (𝓝 (f (x + y))) := by
  rcases hf with ⟨r0, h0⟩
  rcases q.comp_summable_nnreal p hq hp with ⟨r1, r1_pos : 0 < r1, hr1⟩
  let r : ℝ≥0∞ := min r0 r1
  have : EMetric.ballEMetric.ball (0 : E) r ∈ 𝓝 0 :=
    EMetric.ball_mem_nhds 0 (lt_min h0.r_pos (by exact_mod_cast r1_pos))
  filter_upwards [this] with y hy
  have hy0 : y ∈ EMetric.ball 0 r0 := EMetric.ball_subset_ball (min_le_left _ _) hy
  have A : HasSum (fun i : Σ n, Composition n => q.compAlongComposition p i.2 fun _j => y)
      (f (x + y)) := by
    have cau : CauchySeq fun s : Finset (Σ n, Composition n) =>
        ∑ i ∈ s, q.compAlongComposition p i.2 fun _j => y := by
      apply cauchySeq_finset_of_norm_bounded _ (NNReal.summable_coe.2 hr1) _
      simp only [coe_nnnorm, NNReal.coe_mul, NNReal.coe_pow]
      rintro ⟨n, c⟩
      calc
        ‖(compAlongComposition q p c) fun _j : Fin n => y‖ ≤
            ‖compAlongComposition q p c‖ * ∏ _j : Fin n, ‖y‖ := by
          apply ContinuousMultilinearMap.le_opNorm
        _ ≤ ‖compAlongComposition q p c‖ * (r1 : ℝ) ^ n := by
          apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
          rw [Finset.prod_const, Finset.card_fin]
          gcongr
          rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
          have := le_trans (le_of_lt hy) (min_le_right _ _)
          rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
    apply HasSum.of_sigma (fun b ↦ hasSum_fintype _) ?_ cau
    simpa [FormalMultilinearSeries.comp] using h0.hasSum hy0
  have B : Tendsto (fun (n : ℕℕ × ℕ) => ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
      q.compAlongComposition p i.2 fun _j => y) atTop (𝓝 (f (x + y))) := by
    apply Tendsto.comp A compPartialSumTarget_tendsto_prod_atTop
  have C : Tendsto (fun (n : ℕℕ × ℕ) => q.partialSum n.1 (∑ a ∈ Finset.Ico 1 n.2, p a fun _b ↦ y))
      atTop (𝓝 (f (x + y))) := by simpa [comp_partialSum] using B
  apply C.congr'
  filter_upwards [Ici_mem_atTop (0, 1)]
  rintro ⟨-, n⟩ ⟨-, (hn : 1 ≤ n)⟩
  congr
  rw [partialSum, eq_sub_iff_add_eq', Finset.range_eq_Ico,
        Finset.sum_eq_sum_Ico_succ_bot hn]
  congr with i
  exact i.elim0

Convergence of Partial Sums for Composition of Power Series

Informal description

Let $f : E \to G$ be a function with a power series expansion at $x \in E$ given by the composition $q \circ p$ of formal multilinear series $q$ (from $F$ to $G$) and $p$ (from $E$ to $F$). If both $q$ and $p$ have positive radii of convergence, then for all $y$ in a neighborhood of $0$, the sequence of partial sums \[ \sum_{k=0}^{M-1} q_k \left( \sum_{i=0}^{N-1} p_i(y, \dots, y) - p_0(0, \dots, 0) \right) \] converges to $f(x + y)$ as $M, N \to \infty$.

HasFPowerSeriesAt.eventually_hasSum_of_comp theorem

 {f : E → F} {g : F → G} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
  (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x) (hf : HasFPowerSeriesAt f p x) (hq : 0 < q.radius) :
  ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y)))

Full source

lemma HasFPowerSeriesAt.eventually_hasSum_of_comp  {f : E → F} {g : F → G}
    {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (hgf : HasFPowerSeriesAt (g ∘ f) (q.comp p) x) (hf : HasFPowerSeriesAt f p x)
    (hq : 0 < q.radius) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => q n fun _ : Fin n => (f (x + y) - f x)) (g (f (x + y))) := by
  have : ∀ᶠ y in 𝓝 (0 : E), f (x + y) - f x ∈ EMetric.ball 0 q.radius := by
    have A : ContinuousAt (fun y ↦ f (x + y) - f x) 0 := by
      apply ContinuousAt.sub _ continuousAt_const
      exact hf.continuousAt.comp_of_eq (continuous_add_left x).continuousAt (by simp)
    have B : EMetric.ballEMetric.ball 0 q.radius ∈ 𝓝 (f (x + 0) - f x) := by
      simpa using EMetric.ball_mem_nhds _ hq
    exact A.preimage_mem_nhds B
  filter_upwards [hgf.tendsto_partialSum_prod_of_comp hq (hf.radius_pos),
    hf.tendsto_partialSum, this] with y hy h'y h''y
  have L : Tendsto (fun n ↦ q.partialSum n (f (x + y) - f x)) atTop (𝓝 (g (f (x + y)))) := by
    apply (closed_nhds_basis (g (f (x + y)))).tendsto_right_iff.2
    rintro u ⟨hu, u_closed⟩
    simp only [id_eq, eventually_atTop, ge_iff_le]
    rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
    obtain ⟨a₀, b₀, hab⟩ : ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b →
        q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0) ∈ v := by
      simpa using hy (v_open.mem_nhds hv)
    refine ⟨a₀, fun a ha ↦ ?_⟩
    have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0)) atTop
        (𝓝 (q.partialSum a (f (x + y) - f x))) := by
      have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
        (partialSum_continuous q a).continuousAt
      apply this.tendsto.comp
      apply Tendsto.sub h'y
      convert tendsto_const_nhds
      exact (HasFPowerSeriesAt.coeff_zero hf fun _ ↦ 0).symm
    apply u_closed.mem_of_tendsto this
    filter_upwards [Ici_mem_atTop b₀] with b hb using vu (hab _ _ ha hb)
  have C : CauchySeq (fun (s : Finset ℕ) ↦ ∑ n ∈ s, q n fun _ : Fin n => (f (x + y) - f x)) := by
    have Z := q.summable_norm_apply (x := f (x + y) - f x) h''y
    exact cauchySeq_finset_of_norm_bounded _ Z (fun i ↦ le_rfl)
  exact tendsto_nhds_of_cauchySeq_of_subseq C tendsto_finset_range L

Summability of Composition Series for Analytic Functions

Informal description

Let $ f : E \to F $ and $ g : F \to G $ be functions, and let $ p $ and $ q $ be formal multilinear series from $ E $ to $ F $ and from $ F $ to $ G $, respectively. Suppose that: 1. The composition $ g \circ f $ has a power series expansion at $ x \in E $ given by the composition $ q \circ p $. 2. The function $ f $ has a power series expansion at $ x $ given by $ p $. 3. The radius of convergence of $ q $ is positive. Then, for all $ y $ in a neighborhood of $ 0 $, the series $ \sum_{n=0}^\infty q_n(f(x + y) - f(x), \dots, f(x + y) - f(x)) $ converges to $ g(f(x + y)) $.

PartialHomeomorph.hasFPowerSeriesAt_symm theorem

 (f : PartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) {p : FormalMultilinearSeries 𝕜 E F}
  (h : HasFPowerSeriesAt f p a) (hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
  HasFPowerSeriesAt f.symm (p.leftInv i a) (f a)

Full source

/-- If a partial homeomorphism `f` is defined at `a` and has a power series expansion there with
invertible linear term, then `f.symm` has a power series expansion at `f a`, given by the inverse
of the initial power series. -/
theorem PartialHomeomorph.hasFPowerSeriesAt_symm (f : PartialHomeomorph E F) {a : E}
    {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) {p : FormalMultilinearSeries 𝕜 E F}
    (h : HasFPowerSeriesAt f p a) (hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    HasFPowerSeriesAt f.symm (p.leftInv i a) (f a) := by
  have A : HasFPowerSeriesAt (f.symm ∘ f) ((p.leftInv i a).comp p) a := by
    have : HasFPowerSeriesAt (ContinuousLinearMap.id 𝕜 E) ((p.leftInv i a).comp p) a := by
      rw [leftInv_comp _ _ _ hp]
      exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a
    apply this.congr
    filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]
  have B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (a + y) - f a)
      (f.symm (f (a + y))) := by
    simpa using A.eventually_hasSum_of_comp h (radius_leftInv_pos_of_radius_pos h.radius_pos hp)
  have C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a)
      (f.symm (f y)) := by
    rw [← sub_eq_zero_of_eq (a := a) rfl] at B
    have : ContinuousAt (fun x ↦ x - a) a := by fun_prop
    simpa using this.preimage_mem_nhds B
  have D : ∀ᶠ (y : E) in 𝓝 (f.symm (f a)),
      HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f y - f a) y := by
    simp only [h0, PartialHomeomorph.left_inv]
    filter_upwards [C, f.open_source.mem_nhds h0] with x hx h'x
    simpa [h'x] using hx
  have E : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ f (f.symm z) - f a)
      (f.symm z) := by
    have : ContinuousAt f.symm (f a) := f.continuousAt_symm (f.map_source h0)
    exact this D
  have F : ∀ᶠ z in 𝓝 (f a), HasSum (fun n ↦ (p.leftInv i a n) fun _ ↦ z - f a) (f.symm z) := by
    filter_upwards [f.open_target.mem_nhds (f.map_source h0), E] with z hz h'z
    simpa [hz] using h'z
  rcases EMetric.mem_nhds_iff.1 F with ⟨r, r_pos, hr⟩
  refine ⟨min r (p.leftInv i a).radius, min_le_right _ _,
    lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩
  have : y + f a ∈ EMetric.ball (f a) r := by
    simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
      add_sub_cancel_right] at hy ⊢
    exact hy.1
  simpa [add_comm] using hr this

Power Series Expansion of the Inverse of an Analytic Partial Homeomorphism

Informal description

Let $f$ be a partial homeomorphism between normed spaces $E$ and $F$ over a field $\mathbb{K}$, with $a \in f.\text{source}$. Suppose $f$ has a power series expansion at $a$ given by a formal multilinear series $p$ with invertible linear term (i.e., $p_1 = i$ where $i : E \simeq F$ is a continuous linear equivalence). Then the inverse function $f^{-1}$ has a power series expansion at $f(a)$ given by the left inverse series $p.\text{leftInv}\,i\,a$.