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

@[irreducible]

noncomputable def FormalMultilinearSeries.leftInv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 F E

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

Equations

• One or more equations did not get rendered due to their size.
• p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
• p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

@[simp]

theorem FormalMultilinearSeries.leftInv_coeff_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.leftInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

@[simp]

theorem FormalMultilinearSeries.leftInv_coeff_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

theorem FormalMultilinearSeries.leftInv_removeZero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.leftInv i x = p.leftInv i x

The left inverse does not depend on the zeroth coefficient of a formal multilinear series.

theorem FormalMultilinearSeries.leftInv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i) : (p.leftInv i x).comp p = FormalMultilinearSeries.id 𝕜 E x

The left inverse to a formal multilinear series is indeed a left inverse, provided its linear term is invertible.

The right inverse of a formal multilinear series

@[irreducible]

noncomputable def FormalMultilinearSeries.rightInv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 F E

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

Equations

• p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x
• p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
• p.rightInv i x n.succ.succ = -(↑i.symm).compContinuousMultilinearMap (p.comp (fun (k : ℕ) => if k < n + 2 then p.rightInv i x k else 0) (n + 2))

@[simp]

theorem FormalMultilinearSeries.rightInv_coeff_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

@[simp]

theorem FormalMultilinearSeries.rightInv_coeff_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

theorem FormalMultilinearSeries.rightInv_removeZero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.rightInv i x = p.rightInv i x

The right inverse does not depend on the zeroth coefficient of a formal multilinear series.

theorem FormalMultilinearSeries.comp_rightInv_aux1 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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 (x : Fin 1) => (q n) v

theorem FormalMultilinearSeries.comp_rightInv_aux2 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (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) (FormalMultilinearSeries.applyComposition (fun (k : ℕ) => if k < n + 2 then p.rightInv i x k else 0) c v) = ∑ c ∈ {c : Composition (n + 2) | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i x).applyComposition c v)

theorem FormalMultilinearSeries.comp_rightInv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i) : p.comp (p.rightInv i x) = FormalMultilinearSeries.id 𝕜 F ((p 0) 0)

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 FormalMultilinearSeries.rightInv_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (n : ℕ) (hn : 2 ≤ n) : p.rightInv i x n = -(↑i.symm).compContinuousMultilinearMap (∑ c ∈ {c : Composition n | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)

Coincidence of the left and the right inverse

theorem FormalMultilinearSeries.leftInv_eq_rightInv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i) : p.leftInv i x = p.rightInv i x

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 $$ q_n = - (p_1)^{-n} \sum_{k=0}^{n-1} \sum_{i_1 + \dotsc + i_k = n} q_k (p_{i_1}, \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 $$ q_n = - (p_1)^{-1} \sum_{k=2}^n \sum_{i_1 + \dotsc + i_k = n} p_k (q_{i_1}, \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 $$ Q_n ≤ C' \sum_{k=2}^n r^k \sum_{i_1 + \dotsc + i_k = n} Q_{i_1} \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 Q_n z^n = Q_1 z + C' \sum_{2 \leq k \leq n} \sum_{i_1 + \dotsc + i_k = n} (r z^{i_1} Q_{i_1}) \dotsm (r z^{i_k} Q_{i_k}) \\ & = Q_1 z + C' \sum_{k = 2}^\infty (\sum_{i_1 \geq 1} r z^{i_1} Q_{i_1}) \dotsm (\sum_{i_k \geq 1} r z^{i_k} Q_{i_k}) \\ & = Q_1 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 $S_n = \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

$$ S_n \leq Q_1 a + C' \sum_{k=2}^n (r S_{n-1})^k. $$

In particular, $S_n \leq Q_1 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 $S_n \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.

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

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 FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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 ∈ Finset.Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤ ‖↑i.symm‖ * a + ‖↑i.symm‖ * C * ∑ k ∈ Finset.Ico 2 (n + 1), (r * ∑ j ∈ Finset.Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k

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 FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E} (hp : 0 < p.radius) : 0 < (p.rightInv i x).radius

If a a formal multilinear series has a positive radius of convergence, then its right inverse also has a positive radius of convergence.

theorem FormalMultilinearSeries.radius_leftInv_pos_of_radius_pos {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {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

If a a formal multilinear series has a positive radius of convergence, then its left inverse also has a positive radius of convergence.

The inverse of an analytic partial homeomorphism is analytic

theorem HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {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 : E) in nhds 0, Filter.Tendsto (fun (a : ℕ × ℕ) => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun (x : Fin 0) => 0)) Filter.atTop (nhds (f (x + y)))

theorem HasFPowerSeriesAt.eventually_hasSum_of_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {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 : E) in nhds 0, HasSum (fun (n : ℕ) => (q n) fun (x_1 : Fin n) => f (x + y) - f x) (g (f (x + y)))

theorem PartialHomeomorph.hasFPowerSeriesAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (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)

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.