From c70feebd43e143d81a695f7d7e5b21e5892286e8 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 11 Feb 2021 00:37:02 +0000 Subject: [PATCH] feat(analysis/analytic/inverse): convergence of the inverse of a power series (#5854) If a formal multilinear series has a positive radius of convergence, then its inverse also does. --- docs/references.bib | 9 + src/algebra/geom_sum.lean | 4 + src/analysis/analytic/basic.lean | 12 + src/analysis/analytic/composition.lean | 2 +- src/analysis/analytic/inverse.lean | 269 ++++++++++++++++++++- src/analysis/normed_space/multilinear.lean | 41 ++++ 6 files changed, 335 insertions(+), 2 deletions(-) diff --git a/docs/references.bib b/docs/references.bib index af9e2cdd834b9..fde78ec84a846 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -178,6 +178,15 @@ @inproceedings{lewis2019 keywords = {Hensel's lemma, Lean, formal proof, p-adic}, } +@misc{pöschel2017siegelsternberg, + title={On the Siegel-Sternberg linearization theorem}, + author={Jürgen Pöschel}, + year={2017}, + eprint={1702.03691}, + archivePrefix={arXiv}, + primaryClass={math.DS} +} + @book {riehl2017, AUTHOR = {Riehl, Emily}, TITLE = {Category theory in context}, diff --git a/src/algebra/geom_sum.lean b/src/algebra/geom_sum.lean index 0db482996f9f9..7ace94554e033 100644 --- a/src/algebra/geom_sum.lean +++ b/src/algebra/geom_sum.lean @@ -272,6 +272,10 @@ theorem geom_sum_Ico [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn by simp only [sum_Ico_eq_sub _ hmn, (geom_series_def _ _).symm, geom_sum hx, div_sub_div_same, sub_sub_sub_cancel_right] +theorem geom_sum_Ico' [division_ring α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) : + ∑ i in finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x) := +by { simp only [geom_sum_Ico hx hmn], convert neg_div_neg_eq (x^m - x^n) (1-x); abel } + lemma geom_sum_inv [division_ring α] {x : α} (hx1 : x ≠ 1) (hx0 : x ≠ 0) (n : ℕ) : (geom_series x⁻¹ n) = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x) := have h₁ : x⁻¹ ≠ 1, by rwa [inv_eq_one_div, ne.def, div_eq_iff_mul_eq hx0, one_mul], diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean index bb02eaffddf97..92c3ea3d40bea 100644 --- a/src/analysis/analytic/basic.lean +++ b/src/analysis/analytic/basic.lean @@ -182,6 +182,18 @@ lemma nnnorm_mul_pow_le_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h in ⟨⟨C, hC.lt.le⟩, hC, by exact_mod_cast hp⟩ +/-- If the radius of `p` is positive, then `∥pₙ∥` grows at most geometrically. -/ +lemma le_mul_pow_of_radius_pos (p : formal_multilinear_series 𝕜 E F) (h : 0 < p.radius) : + ∃ C r (hC : 0 < C) (hr : 0 < r), ∀ n, ∥p n∥ ≤ C * r ^ n := +begin + rcases ennreal.lt_iff_exists_nnreal_btwn.1 h with ⟨r, r0, rlt⟩, + have rpos : 0 < (r : ℝ), by simp [ennreal.coe_pos.1 r0], + rcases norm_le_div_pow_of_pos_of_lt_radius p rpos rlt with ⟨C, Cpos, hCp⟩, + refine ⟨C, r ⁻¹, Cpos, by simp [rpos], λ n, _⟩, + convert hCp n, + exact inv_pow' _ _, +end + /-- The radius of the sum of two formal series is at least the minimum of their two radii. -/ lemma min_radius_le_radius_add (p q : formal_multilinear_series 𝕜 E F) : min p.radius q.radius ≤ (p + q).radius := diff --git a/src/analysis/analytic/composition.lean b/src/analysis/analytic/composition.lean index dc57320744d61..e0988d18102d6 100644 --- a/src/analysis/analytic/composition.lean +++ b/src/analysis/analytic/composition.lean @@ -457,7 +457,7 @@ begin ... ≤ Cq : hCq _, have B, calc ((∏ i, nnnorm (p (c.blocks_fun i))) * rp ^ n) - ≤ ∏ i, nnnorm (p (c.blocks_fun i)) * rp ^ c.blocks_fun i : + = ∏ i, nnnorm (p (c.blocks_fun i)) * rp ^ c.blocks_fun i : by simp only [finset.prod_mul_distrib, finset.prod_pow_eq_pow_sum, c.sum_blocks_fun] ... ≤ ∏ i : fin c.length, Cp : finset.prod_le_prod' (λ i _, hCp _) ... = Cp ^ c.length : by simp diff --git a/src/analysis/analytic/inverse.lean b/src/analysis/analytic/inverse.lean index be3f5a29acbff..3ea741c9d1fcb 100644 --- a/src/analysis/analytic/inverse.lean +++ b/src/analysis/analytic/inverse.lean @@ -10,7 +10,7 @@ import analysis.analytic.composition # Inverse of analytic functions We construct the left and right inverse of a formal multilinear series with invertible linear term, -and we prove that they coincide. +we prove that they coincide and study their properties (notably convergence). ## Main statements @@ -21,6 +21,8 @@ and we prove that they coincide. * `p.left_inv_comp` says that `p.left_inv i` is indeed a left inverse to `p` when `p₁ = i`. * `p.right_inv_comp` says that `p.right_inv i` is indeed a right inverse to `p` when `p₁ = i`. * `p.left_inv_eq_right_inv`: the two inverses coincide. +* `p.radius_right_inv_pos_of_radius_pos`: if a power series has a positive radius of convergence, + then so does its inverse. -/ @@ -268,4 +270,269 @@ left_inv p i = left_inv p.remove_zero i : by rw left_inv_remove_zero ... = right_inv p.remove_zero i : by { apply left_inv_eq_right_inv_aux; simp [h] } ... = right_inv p i : by rw right_inv_remove_zero +/-! +### 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 [pöschel2017siegelsternberg]. 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. +-/ + +/-- First technical lemma to control the growth of coefficients of the inverse. Bound the explicit +expression for `∑_{k