From 0830bfd44ab1234510700793626ed4eda77a5085 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 31 Dec 2020 16:30:28 +0000 Subject: [PATCH] refactor(analysis/analytic/basic): redefine `formal_multilinear_series.radius` (#5349) With the new definition, (a) some proofs get much shorter; (b) we don't need `rpow` in `analytic/basic`. --- src/algebra/big_operators/order.lean | 1 - src/analysis/analytic/basic.lean | 326 ++++++++++------------- src/analysis/analytic/composition.lean | 161 ++++------- src/analysis/analytic/radius_liminf.lean | 53 ++++ src/analysis/specific_limits.lean | 13 +- 5 files changed, 264 insertions(+), 290 deletions(-) create mode 100644 src/analysis/analytic/radius_liminf.lean diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean index c743c181fbcdf..83267250cfed5 100644 --- a/src/algebra/big_operators/order.lean +++ b/src/algebra/big_operators/order.lean @@ -245,7 +245,6 @@ prod_induction f (λ x, 0 ≤ x) (λ _ _ ha hb, mul_nonneg ha hb) zero_le_one h0 lemma prod_pos {s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < (∏ x in s, f x) := prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0 - /- this is also true for a ordered commutative multiplicative monoid -/ lemma prod_le_prod {s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x) (h1 : ∀(x ∈ s), f x ≤ g x) : (∏ x in s, f x) ≤ (∏ x in s, g x) := diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean index 72a9226eaf597..a652781d74e51 100644 --- a/src/analysis/analytic/basic.lean +++ b/src/analysis/analytic/basic.lean @@ -1,11 +1,10 @@ /- Copyright (c) 2020 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sébastien Gouëzel +Authors: Sébastien Gouëzel, Yury Kudryashov -/ -import analysis.calculus.times_cont_diff -import tactic.omega -import analysis.special_functions.pow +import analysis.calculus.formal_multilinear_series +import analysis.specific_limits /-! # Analytic functions @@ -29,8 +28,13 @@ for `n : ℕ`. * `p.radius`: the largest `r : ennreal` such that `∥p n∥ * r^n` grows subexponentially, defined as a liminf. -* `p.le_radius_of_bound`, `p.bound_of_lt_radius`, `p.geometric_bound_of_lt_radius`: relating the - value of the radius with the growth of `∥p n∥ * r^n`. +* `p.le_radius_of_bound`, `p.le_radius_of_bound_nnreal`, `p.le_radius_of_is_O`: if `∥p n∥ * r ^ n` + is bounded above, then `r ≤ p.radius`; +* `p.is_o_of_lt_radius`, `p.norm_mul_pow_le_mul_pow_of_lt_radius`, `p.is_o_one_of_lt_radius`, + `p.norm_mul_pow_le_of_lt_radius`, `p.nnnorm_mul_pow_le_of_lt_radius`: if `r < p.radius`, then + `∥p n∥ * r ^ n` tends to zero exponentially; +* `p.lt_radius_of_is_O`: if `r ≠ 0` and `∥p n∥ * r ^ n = O(a ^ n)` for some `-1 < a < 1`, then + `r < p.radius`; * `p.partial_sum n x`: the sum `∑_{i = 0}^{n-1} pᵢ xⁱ`. * `p.sum x`: the sum `∑'_{i = 0}^{∞} pᵢ xⁱ`. @@ -70,119 +74,115 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {G : Type*} [normed_group G] [normed_space 𝕜 G] open_locale topological_space classical big_operators nnreal -open filter +open set filter asymptotics /-! ### The radius of a formal multilinear series -/ namespace formal_multilinear_series +variables (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} + /-- The radius of a formal multilinear series is the largest `r` such that the sum `Σ pₙ yⁿ` converges for all `∥y∥ < r`. -/ def radius (p : formal_multilinear_series 𝕜 E F) : ennreal := -liminf at_top (λ n, 1/((nnnorm (p n)) ^ (1 / (n : ℝ)) : ℝ≥0)) +⨆ (r : ℝ≥0) (C : ℝ) (hr : ∀ n, ∥p n∥ * r ^ n ≤ C), (r : ennreal) + +/-- If `∥pₙ∥ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/ +lemma le_radius_of_bound (p : formal_multilinear_series 𝕜 E F) (C : ℝ) {r : ℝ≥0} + (h : ∀ (n : ℕ), ∥p n∥ * r^n ≤ C) : (r : ennreal) ≤ p.radius := +le_supr_of_le r $ le_supr_of_le C $ (le_supr (λ _, (r : ennreal)) h) -/--If `∥pₙ∥ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/ -lemma le_radius_of_bound (p : formal_multilinear_series 𝕜 E F) (C : ℝ≥0) {r : ℝ≥0} +/-- If `∥pₙ∥ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/ +lemma le_radius_of_bound_nnreal (p : formal_multilinear_series 𝕜 E F) (C : ℝ≥0) {r : ℝ≥0} (h : ∀ (n : ℕ), nnnorm (p n) * r^n ≤ C) : (r : ennreal) ≤ p.radius := +p.le_radius_of_bound C $ λ n, by exact_mod_cast (h n) + +/-- If `∥pₙ∥ rⁿ = O(1)`, as `n → ∞`, then the radius of `p` is at least `r`. -/ +lemma le_radius_of_is_O (h : is_O (λ n, ∥p n∥ * r^n) (λ n, (1 : ℝ)) at_top) : ↑r ≤ p.radius := +exists.elim (is_O_one_nat_at_top_iff.1 h) $ λ C hC, p.le_radius_of_bound C $ + λ n, (le_abs_self _).trans (hC n) + +/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially: +for some `0 < a < 1`, `∥p n∥ rⁿ = o(aⁿ)`. -/ +lemma is_o_of_lt_radius (h : ↑r < p.radius) : + ∃ a ∈ Ioo (0 : ℝ) 1, is_o (λ n, ∥p n∥ * r ^ n) (pow a) at_top := begin - have L : tendsto (λ n : ℕ, (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : ℝ≥0)) - at_top (𝓝 ((r : ennreal) / ((C + 1)^(0 : ℝ) : ℝ≥0))), - { apply ennreal.tendsto.div tendsto_const_nhds, - { simp }, - { rw ennreal.tendsto_coe, - apply tendsto_const_nhds.nnrpow (tendsto_const_div_at_top_nhds_0_nat 1), - simp }, - { simp } }, - have A : ∀ n : ℕ , 0 < n → - (r : ennreal) ≤ ((C + 1)^(1/(n : ℝ)) : ℝ≥0) * (1 / (nnnorm (p n) ^ (1/(n:ℝ)) : ℝ≥0)), - { assume n npos, - simp only [one_div, mul_assoc, mul_one, eq.symm ennreal.mul_div_assoc], - rw [ennreal.le_div_iff_mul_le _ _, ← nnreal.pow_nat_rpow_nat_inv r npos, ← ennreal.coe_mul, - ennreal.coe_le_coe, ← nnreal.mul_rpow, mul_comm], - { exact nnreal.rpow_le_rpow (le_trans (h n) (le_add_right (le_refl _))) (by simp) }, - { simp }, - { simp } }, - have B : ∀ᶠ (n : ℕ) in at_top, - (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : ℝ≥0) ≤ 1 / (nnnorm (p n) ^ (1/(n:ℝ)) : ℝ≥0), - { apply eventually_at_top.2 ⟨1, λ n hn, _⟩, - rw [ennreal.div_le_iff_le_mul, mul_comm], - { apply A n hn }, - { simp }, - { simp } }, - have D : liminf at_top (λ n : ℕ, (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : ℝ≥0)) ≤ p.radius := - liminf_le_liminf B, - rw L.liminf_eq at D, - simpa using D + rw (tfae_exists_lt_is_o_pow (λ n, ∥p n∥ * r ^ n) 1).out 1 4, + simp only [radius, lt_supr_iff] at h, + rcases h with ⟨t, C, hC, rt⟩, + rw [ennreal.coe_lt_coe, ← nnreal.coe_lt_coe] at rt, + have : 0 < (t : ℝ), from r.coe_nonneg.trans_lt rt, + rw [← div_lt_one this] at rt, + refine ⟨_, rt, C, or.inr zero_lt_one, λ n, _⟩, + calc abs (∥p n∥ * r ^ n) = (∥p n∥ * t ^ n) * (r / t) ^ n : + by field_simp [mul_right_comm, abs_mul, this.ne'] + ... ≤ C * (r / t) ^ n : mul_le_mul_of_nonneg_right (hC n) (pow_nonneg (div_nonneg r.2 t.2) _) end -/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` is bounded. -/ -lemma bound_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} - (h : (r : ennreal) < p.radius) : ∃ (C : ℝ≥0), ∀ n, nnnorm (p n) * r^n ≤ C := +/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ = o(1)`. -/ +lemma is_o_one_of_lt_radius (h : ↑r < p.radius) : + is_o (λ n, ∥p n∥ * r ^ n) (λ _, 1 : ℕ → ℝ) at_top := +let ⟨a, ha, hp⟩ := p.is_o_of_lt_radius h in +hp.trans $ (is_o_pow_pow_of_lt_left ha.1.le ha.2).congr (λ n, rfl) one_pow + +/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially: +for some `0 < a < 1` and `C > 0`, `∥p n∥ * r ^ n ≤ C * a ^ n`. -/ +lemma norm_mul_pow_le_mul_pow_of_lt_radius (h : ↑r < p.radius) : + ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), ∀ n, ∥p n∥ * r^n ≤ C * a^n := begin - obtain ⟨N, hN⟩ : ∃ (N : ℕ), ∀ n, n ≥ N → (r : ennreal) < 1 / ↑(nnnorm (p n) ^ (1 / (n : ℝ))) := - eventually.exists_forall_of_at_top (eventually_lt_of_lt_liminf h), - obtain ⟨D, hD⟩ : ∃D, ∀ x ∈ (↑((finset.range N.succ).image (λ i, nnnorm (p i) * r^i))), x ≤ D := - finset.bdd_above _, - refine ⟨max D 1, λ n, _⟩, - cases le_or_lt n N with hn hn, - { refine le_trans _ (le_max_left D 1), - apply hD, - have : n ∈ finset.range N.succ := list.mem_range.mpr (nat.lt_succ_iff.mpr hn), - exact finset.mem_image_of_mem _ this }, - { by_cases hpn : nnnorm (p n) = 0, { simp [hpn] }, - have A : nnnorm (p n) ^ (1 / (n : ℝ)) ≠ 0, by simp [nnreal.rpow_eq_zero_iff, hpn], - have B : r < (nnnorm (p n) ^ (1 / (n : ℝ)))⁻¹, - { have := hN n (le_of_lt hn), - rwa [ennreal.div_def, ← ennreal.coe_inv A, one_mul, ennreal.coe_lt_coe] at this }, - rw [nnreal.lt_inv_iff_mul_lt A, mul_comm] at B, - have : (nnnorm (p n) ^ (1 / (n : ℝ)) * r) ^ n ≤ 1 := - pow_le_one n (zero_le (nnnorm (p n) ^ (1 / ↑n) * r)) (le_of_lt B), - rw [mul_pow, one_div, nnreal.rpow_nat_inv_pow_nat _ (lt_of_le_of_lt (zero_le _) hn)] - at this, - exact le_trans this (le_max_right _ _) }, + rcases ((tfae_exists_lt_is_o_pow (λ n, ∥p n∥ * r ^ n) 1).out 1 5).mp (p.is_o_of_lt_radius h) + with ⟨a, ha, C, hC, H⟩, + exact ⟨a, ha, C, hC, λ n, (le_abs_self _).trans (H n)⟩ end -/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially. -/ -lemma geometric_bound_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} - (h : (r : ennreal) < p.radius) : ∃ a C, a < 1 ∧ ∀ n, nnnorm (p n) * r^n ≤ C * a^n := +/-- If `r ≠ 0` and `∥pₙ∥ rⁿ = O(aⁿ)` for some `-1 < a < 1`, then `r < p.radius`. -/ +lemma lt_radius_of_is_O (h₀ : r ≠ 0) {a : ℝ} (ha : a ∈ Ioo (-1 : ℝ) 1) + (hp : is_O (λ n, ∥p n∥ * r ^ n) (pow a) at_top) : + ↑r < p.radius := begin - obtain ⟨t, rt, tp⟩ : ∃ (t : ℝ≥0), (r : ennreal) < t ∧ (t : ennreal) < p.radius := - ennreal.lt_iff_exists_nnreal_btwn.1 h, - rw ennreal.coe_lt_coe at rt, - have tpos : t ≠ 0 := ne_of_gt (lt_of_le_of_lt (zero_le _) rt), - obtain ⟨C, hC⟩ : ∃ (C : ℝ≥0), ∀ n, nnnorm (p n) * t^n ≤ C := p.bound_of_lt_radius tp, - refine ⟨r / t, C, nnreal.div_lt_one_of_lt rt, λ n, _⟩, - calc nnnorm (p n) * r ^ n - = (nnnorm (p n) * t ^ n) * (r / t) ^ n : by { field_simp [tpos], ac_refl } - ... ≤ C * (r / t) ^ n : mul_le_mul_of_nonneg_right (hC n) (zero_le _) + rcases ((tfae_exists_lt_is_o_pow (λ n, ∥p n∥ * r ^ n) 1).out 2 5).mp ⟨a, ha, hp⟩ + with ⟨a, ha, C, hC, hp⟩, + replace h₀ : 0 < r := zero_lt_iff_ne_zero.2 h₀, + lift a to ℝ≥0 using ha.1.le, + have : (r : ℝ) < r / a := + (lt_div_iff ha.1).2 (by simpa only [mul_one] using mul_lt_mul_of_pos_left ha.2 h₀), + norm_cast at this, + rw [← ennreal.coe_lt_coe] at this, + refine this.trans_le (p.le_radius_of_bound C $ λ n, _), + rw [nnreal.coe_div, div_pow, ← mul_div_assoc, div_le_iff (pow_pos ha.1 n)], + exact (le_abs_self _).trans (hp n) end +/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` is bounded. -/ +lemma norm_mul_pow_le_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} + (h : (r : ennreal) < p.radius) : ∃ C > 0, ∀ n, ∥p n∥ * r^n ≤ C := +let ⟨a, ha, C, hC, h⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h +in ⟨C, hC, λ n, (h n).trans $ mul_le_of_le_one_right hC.lt.le (pow_le_one _ ha.1.le ha.2.le)⟩ + +/-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` is bounded. -/ +lemma nnnorm_mul_pow_le_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0} + (h : (r : ennreal) < p.radius) : ∃ C > 0, ∀ n, nnnorm (p n) * r^n ≤ C := +let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h +in ⟨⟨C, hC.lt.le⟩, hC, by exact_mod_cast hp⟩ + /-- 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 := begin - refine le_of_forall_ge_of_dense (λ r hr, _), - cases r, { simpa using hr }, - obtain ⟨Cp, hCp⟩ : ∃ (C : ℝ≥0), ∀ n, nnnorm (p n) * r^n ≤ C := - p.bound_of_lt_radius (lt_of_lt_of_le hr (min_le_left _ _)), - obtain ⟨Cq, hCq⟩ : ∃ (C : ℝ≥0), ∀ n, nnnorm (q n) * r^n ≤ C := - q.bound_of_lt_radius (lt_of_lt_of_le hr (min_le_right _ _)), - have : ∀ n, nnnorm ((p + q) n) * r^n ≤ Cp + Cq, - { assume n, - calc nnnorm (p n + q n) * r ^ n - ≤ (nnnorm (p n) + nnnorm (q n)) * r ^ n : - mul_le_mul_of_nonneg_right (norm_add_le (p n) (q n)) (zero_le (r ^ n)) - ... ≤ Cp + Cq : by { rw add_mul, exact add_le_add (hCp n) (hCq n) } }, - exact (p + q).le_radius_of_bound _ this + refine ennreal.le_of_forall_nnreal_lt (λ r hr, _), + rw lt_min_iff at hr, + have := ((p.is_o_one_of_lt_radius hr.1).add (q.is_o_one_of_lt_radius hr.2)).is_O, + refine (p + q).le_radius_of_is_O ((is_O_of_le _ $ λ n, _).trans this), + rw [← add_mul, normed_field.norm_mul, normed_field.norm_mul, norm_norm], + exact mul_le_mul_of_nonneg_right ((norm_add_le _ _).trans (le_abs_self _)) (norm_nonneg _) end -lemma radius_neg (p : formal_multilinear_series 𝕜 E F) : (-p).radius = p.radius := -by simp [formal_multilinear_series.radius, nnnorm_neg] +@[simp] lemma radius_neg (p : formal_multilinear_series 𝕜 E F) : (-p).radius = p.radius := +by simp [radius] /-- Given a formal multilinear series `p` and a vector `x`, then `p.sum x` is the sum `Σ pₙ xⁿ`. A priori, it only behaves well when `∥x∥ < p.radius`. -/ -protected def sum (p : formal_multilinear_series 𝕜 E F) (x : E) : F := -tsum (λn:ℕ, p n (λ(i : fin n), x)) +protected def sum (p : formal_multilinear_series 𝕜 E F) (x : E) : F := ∑' n : ℕ , p n (λ i, x) /-- Given a formal multilinear series `p` and a vector `x`, then `p.partial_sum n x` is the sum `Σ pₖ xᵏ` for `k ∈ {0,..., n-1}`. -/ @@ -196,14 +196,14 @@ by continuity end formal_multilinear_series - /-! ### Expanding a function as a power series -/ section variables {f g : E → F} {p pf pg : formal_multilinear_series 𝕜 E F} {x : E} {r r' : ennreal} /-- Given a function `f : E → F` and a formal multilinear series `p`, we say that `f` has `p` as -a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `∥y∥ < r`. -/ +a power series on the ball of radius `r > 0` around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `∥y∥ < r`. +-/ structure has_fpower_series_on_ball (f : E → F) (p : formal_multilinear_series 𝕜 E F) (x : E) (r : ennreal) : Prop := (r_le : r ≤ p.radius) @@ -297,13 +297,12 @@ by simpa only [sub_eq_add_neg] using hf.add hg.neg lemma has_fpower_series_on_ball.coeff_zero (hf : has_fpower_series_on_ball f pf x r) (v : fin 0 → E) : pf 0 v = f x := begin - have v_eq : v = (λ i, 0), by { ext i, apply fin_zero_elim i }, + have v_eq : v = (λ i, 0) := subsingleton.elim _ _, have zero_mem : (0 : E) ∈ emetric.ball (0 : E) r, by simp [hf.r_pos], have : ∀ i ≠ 0, pf i (λ j, 0) = 0, { assume i hi, - have : 0 < i := bot_lt_iff_ne_bot.mpr hi, - apply continuous_multilinear_map.map_coord_zero _ (⟨0, this⟩ : fin i), - refl }, + have : 0 < i := zero_lt_iff_ne_zero.2 hi, + exact continuous_multilinear_map.map_coord_zero _ (⟨0, this⟩ : fin i) rfl }, have A := (hf.has_sum zero_mem).unique (has_sum_single _ this), simpa [v_eq] using A.symm, end @@ -316,29 +315,25 @@ let ⟨rf, hrf⟩ := hf in hrf.coeff_zero v sums of this power series on strict subdisks of the disk of convergence. -/ lemma has_fpower_series_on_ball.uniform_geometric_approx {r' : ℝ≥0} (hf : has_fpower_series_on_ball f p x r) (h : (r' : ennreal) < r) : - ∃ (a C : ℝ≥0), a < 1 ∧ (∀ y ∈ metric.ball (0 : E) r', ∀ n, + ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), (∀ y ∈ metric.ball (0 : E) r', ∀ n, ∥f (x + y) - p.partial_sum n y∥ ≤ C * a ^ n) := begin - obtain ⟨a, C, ha, hC⟩ : ∃ a C, a < 1 ∧ ∀ n, nnnorm (p n) * r' ^n ≤ C * a^n := - p.geometric_bound_of_lt_radius (lt_of_lt_of_le h hf.r_le), - refine ⟨a, C / (1 - a), ha, λ y hy n, _⟩, + obtain ⟨a, ha, C, hC, hp⟩ : ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), ∀ n, ∥p n∥ * r' ^n ≤ C * a^n := + p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le), + refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), λ y hy n, _⟩, have yr' : ∥y∥ < r', by { rw ball_0_eq at hy, exact hy }, have : y ∈ emetric.ball (0 : E) r, - { rw [emetric.mem_ball, edist_eq_coe_nnnorm], - apply lt_trans _ h, - rw [ennreal.coe_lt_coe, ← nnreal.coe_lt_coe], - exact yr' }, - simp only [nnreal.coe_sub (le_of_lt ha), nnreal.coe_sub, nnreal.coe_div, nnreal.coe_one], - rw [← dist_eq_norm, dist_comm, dist_eq_norm, ← mul_div_right_comm], - apply norm_sub_le_of_geometric_bound_of_has_sum ha _ (hf.has_sum this), + { refine mem_emetric_ball_0_iff.2 (lt_trans _ h), + exact_mod_cast yr' }, + rw [norm_sub_rev, ← mul_div_right_comm], + apply norm_sub_le_of_geometric_bound_of_has_sum ha.2 _ (hf.has_sum this), assume n, - calc ∥(p n) (λ (i : fin n), y)∥ - ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) : continuous_multilinear_map.le_op_norm _ _ - ... = nnnorm (p n) * (nnnorm y)^n : by simp - ... ≤ nnnorm (p n) * r' ^ n : - mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left (nnreal.coe_nonneg _) (le_of_lt yr') _) - (nnreal.coe_nonneg _) - ... ≤ C * a ^ n : by exact_mod_cast hC n, + calc ∥(p n) (λ (i : fin n), y)∥ ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) : + continuous_multilinear_map.le_op_norm _ _ + ... = ∥p n∥ * ∥y∥ ^ n : by simp + ... ≤ ∥p n∥ * r' ^ n : + mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left (norm_nonneg _) yr'.le _) (norm_nonneg _) + ... ≤ C * a ^ n : hp n end /-- If a function admits a power series expansion at `x`, then it is the uniform limit of the @@ -346,17 +341,17 @@ partial sums of this power series on strict subdisks of the disk of convergence, is the uniform limit of `p.partial_sum n y` there. -/ lemma has_fpower_series_on_ball.tendsto_uniformly_on {r' : ℝ≥0} (hf : has_fpower_series_on_ball f p x r) (h : (r' : ennreal) < r) : - tendsto_uniformly_on (λ n y, p.partial_sum n y) (λ y, f (x + y)) at_top (metric.ball (0 : E) r') := + tendsto_uniformly_on (λ n y, p.partial_sum n y) + (λ y, f (x + y)) at_top (metric.ball (0 : E) r') := begin - rcases hf.uniform_geometric_approx h with ⟨a, C, ha, hC⟩, + rcases hf.uniform_geometric_approx h with ⟨a, ha, C, hC, hp⟩, refine metric.tendsto_uniformly_on_iff.2 (λ ε εpos, _), have L : tendsto (λ n, (C : ℝ) * a^n) at_top (𝓝 ((C : ℝ) * 0)) := - tendsto_const_nhds.mul (tendsto_pow_at_top_nhds_0_of_lt_1 (a.2) ha), + tendsto_const_nhds.mul (tendsto_pow_at_top_nhds_0_of_lt_1 ha.1.le ha.2), rw mul_zero at L, - apply ((tendsto_order.1 L).2 ε εpos).mono (λ n hn, _), - assume y hy, + refine (L.eventually (gt_mem_nhds εpos)).mono (λ n hn y hy, _), rw dist_eq_norm, - exact lt_of_le_of_lt (hC y hy n) hn + exact (hp y hy n).trans_lt hn end /-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of @@ -365,7 +360,7 @@ is the locally uniform limit of `p.partial_sum n y` there. -/ lemma has_fpower_series_on_ball.tendsto_locally_uniformly_on (hf : has_fpower_series_on_ball f p x r) : tendsto_locally_uniformly_on (λ n y, p.partial_sum n y) (λ y, f (x + y)) - at_top (emetric.ball (0 : E) r) := + at_top (emetric.ball (0 : E) r) := begin assume u hu x hx, rcases ennreal.lt_iff_exists_nnreal_btwn.1 hx with ⟨r', xr', hr'⟩, @@ -383,7 +378,7 @@ lemma has_fpower_series_on_ball.tendsto_uniformly_on' {r' : ℝ≥0} tendsto_uniformly_on (λ n y, p.partial_sum n (y - x)) f at_top (metric.ball (x : E) r') := begin convert (hf.tendsto_uniformly_on h).comp (λ y, y - x), - { ext z, simp }, + { simp [(∘)] }, { ext z, simp [dist_eq_norm] } end @@ -424,14 +419,14 @@ lemma formal_multilinear_series.has_fpower_series_on_ball [complete_space F] rw zero_add, replace hy : (nnnorm y : ennreal) < p.radius, by { convert hy, exact (edist_eq_coe_nnnorm _).symm }, - obtain ⟨a, C, ha, hC⟩ : ∃ a C, a < 1 ∧ ∀ n, nnnorm (p n) * (nnnorm y)^n ≤ C * a^n := - p.geometric_bound_of_lt_radius hy, + obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, hC : 0 < C, hp⟩ := + p.norm_mul_pow_le_mul_pow_of_lt_radius hy, refine (summable_of_norm_bounded (λ n, (C : ℝ) * a ^ n) - ((summable_geometric_of_lt_1 a.2 ha).mul_left _) (λ n, _)).has_sum, + ((summable_geometric_of_lt_1 ha.1.le ha.2).mul_left _) (λ n, _)).has_sum, calc ∥(p n) (λ (i : fin n), y)∥ ≤ ∥p n∥ * (∏ i : fin n, ∥y∥) : continuous_multilinear_map.le_op_norm _ _ - ... = nnnorm (p n) * (nnnorm y)^n : by simp - ... ≤ C * a ^ n : by exact_mod_cast hC n + ... = ∥p n∥ * (nnnorm y)^n : by simp + ... ≤ C * a ^ n : hp n end } lemma has_fpower_series_on_ball.sum [complete_space F] (h : has_fpower_series_on_ball f p x r) @@ -446,10 +441,9 @@ end lemma formal_multilinear_series.continuous_on [complete_space F] : continuous_on p.sum (emetric.ball 0 p.radius) := begin - by_cases h : 0 < p.radius, - { exact (p.has_fpower_series_on_ball h).continuous_on }, - { simp at h, - simp [h, continuous_on_empty] } + cases (zero_le p.radius).eq_or_lt with h h, + { simp [← h, continuous_on_empty] }, + { exact (p.has_fpower_series_on_ball h).continuous_on } end end @@ -487,10 +481,8 @@ as this leads to a bad definition with auxiliary `_match` statements, but we will try to use pattern matching in lambdas as much as possible in the proofs below to increase readability. -/ -def change_origin (x : E) : - formal_multilinear_series 𝕜 E F := -λ k, tsum (λi, (p i.1).restr i.2.1 i.2.2 x : - (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → (E [×k]→L[𝕜] F)) +def change_origin (x : E) : formal_multilinear_series 𝕜 E F := +λ k, ∑' i : Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}, (p i.1).restr i.2 i.2.2 x /-- Auxiliary lemma controlling the summability of the sequence appearing in the definition of `p.change_origin`, first version. -/ @@ -501,34 +493,18 @@ lemma change_origin_summable_aux1 (h : (nnnorm x + r : ennreal) < p.radius) : @summable ℝ _ _ _ ((λ ⟨n, s⟩, ∥p n∥ * ∥x∥ ^ (n - s.card) * r ^ s.card) : (Σ (n : ℕ), finset (fin n)) → ℝ) := begin - obtain ⟨a, C, ha, hC⟩ : - ∃ a C, a < 1 ∧ ∀ n, nnnorm (p n) * (nnnorm x + r) ^ n ≤ C * a^n := - p.geometric_bound_of_lt_radius h, - let Bnnnorm : (Σ (n : ℕ), finset (fin n)) → ℝ≥0 := - λ ⟨n, s⟩, nnnorm (p n) * (nnnorm x) ^ (n - s.card) * r ^ s.card, - have : ((λ ⟨n, s⟩, ∥p n∥ * ∥x∥ ^ (n - s.card) * r ^ s.card) : - (Σ (n : ℕ), finset (fin n)) → ℝ) = (λ b, (Bnnnorm b : ℝ)), - by { ext ⟨n, s⟩, simp [Bnnnorm, nnreal.coe_pow, coe_nnnorm] }, - rw [this, nnreal.summable_coe, ← ennreal.tsum_coe_ne_top_iff_summable], - apply ne_of_lt, - calc (∑' b, ↑(Bnnnorm b)) - = (∑' n, (∑' s, ↑(Bnnnorm ⟨n, s⟩))) : by exact ennreal.tsum_sigma' _ - ... ≤ (∑' n, (((nnnorm (p n) * (nnnorm x + r)^n) : ℝ≥0) : ennreal)) : - begin - refine ennreal.tsum_le_tsum (λ n, _), - rw [tsum_fintype, ← ennreal.coe_finset_sum, ennreal.coe_le_coe], - apply le_of_eq, - calc ∑ s : finset (fin n), Bnnnorm ⟨n, s⟩ - = ∑ s : finset (fin n), nnnorm (p n) * ((nnnorm x) ^ (n - s.card) * r ^ s.card) : - by simp [← mul_assoc] - ... = nnnorm (p n) * (nnnorm x + r) ^ n : - by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr' with s : 1, ring } - end - ... ≤ (∑' (n : ℕ), (C * a ^ n : ennreal)) : - tsum_le_tsum (λ n, by exact_mod_cast hC n) ennreal.summable ennreal.summable - ... < ⊤ : - by simp [ennreal.mul_eq_top, ha, ennreal.tsum_mul_left, ennreal.tsum_geometric, - ennreal.lt_top_iff_ne_top] + obtain ⟨a, ha, C, hC, hp : ∀ n, ∥p n∥ * (∥x∥ + ↑r) ^ n ≤ C * a ^ n⟩ := + p.norm_mul_pow_le_mul_pow_of_lt_radius h, + set B : (Σ n, finset (fin n)) → ℝ := λ ⟨n, s⟩, ∥p n∥ * ∥x∥ ^ (n - s.card) * r ^ s.card, + have H : ∀ n s, 0 ≤ B ⟨n, s⟩ := λ n s, by apply_rules [mul_nonneg, pow_nonneg, norm_nonneg, r.2], + rw summable_sigma_of_nonneg (λ ⟨n, s⟩, H n s), + have : ∀ n, has_sum (λ s, B ⟨n, s⟩) (∥p n∥ * (∥x∥ + r) ^ n), + { simpa only [← fin.sum_pow_mul_eq_add_pow, finset.mul_sum, ← mul_assoc, + add_comm _ ↑r, mul_right_comm] using λ n, has_sum_fintype (λ s, B ⟨n, s⟩) }, + refine ⟨λ n, (this n).summable, _⟩, + simp only [(this _).tsum_eq], + exact summable_of_nonneg_of_le (λ n, (this n).nonneg (H n)) hp + ((summable_geometric_of_lt_1 ha.1.le ha.2).mul_left _) end /-- Auxiliary lemma controlling the summability of the sequence appearing in the definition of @@ -571,7 +547,8 @@ lemma change_origin_summable_aux_j_injective (k : ℕ) : function.injective (change_origin_summable_aux_j k) := begin rintros ⟨_, ⟨_, _⟩⟩ ⟨_, ⟨_, _⟩⟩ a, - simp only [change_origin_summable_aux_j, true_and, eq_self_iff_true, heq_iff_eq, sigma.mk.inj_iff] at a, + simp only [change_origin_summable_aux_j, true_and, eq_self_iff_true, heq_iff_eq, + sigma.mk.inj_iff] at a, rcases a with ⟨rfl, a⟩, simpa using a, end @@ -603,13 +580,11 @@ end convergence.-/ lemma change_origin_radius : p.radius - nnnorm x ≤ (p.change_origin x).radius := begin - by_cases h : p.radius ≤ nnnorm x, + cases le_or_lt p.radius (nnnorm x) with h h, { have : radius p - ↑(nnnorm x) = 0 := ennreal.sub_eq_zero_of_le h, rw this, exact zero_le _ }, - replace h : (nnnorm x : ennreal) < p.radius, by simpa using h, - refine le_of_forall_ge_of_dense (λ r hr, _), - cases r, { simpa using hr }, + refine ennreal.le_of_forall_nnreal_lt (λ r hr, _), rw [ennreal.lt_sub_iff_add_lt, add_comm] at hr, let A : (Σ (k : ℕ) (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ := λ ⟨k, n, s, hs⟩, ∥(p n).restr s hs x∥ * (r : ℝ) ^ k, @@ -619,14 +594,10 @@ begin change 0 ≤ ∥(p n).restr s hs x∥ * (r : ℝ) ^ k, refine mul_nonneg (norm_nonneg _) (pow_nonneg (nnreal.coe_nonneg _) _) }, have tsum_nonneg : 0 ≤ tsum A := tsum_nonneg A_nonneg, - apply le_radius_of_bound _ (nnreal.of_real (tsum A)) (λ k, _), - rw [← nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_pow, coe_nnnorm, - nnreal.coe_of_real _ tsum_nonneg], + refine le_radius_of_bound _ (tsum A) (λ k, _), calc ∥change_origin p x k∥ * ↑r ^ k - = ∥@tsum (E [×k]→L[𝕜] F) _ _ _ (λ i, (p i.1).restr i.2.1 i.2.2 x : - (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → (E [×k]→L[𝕜] F))∥ * ↑r ^ k : rfl - ... ≤ tsum (λ i, ∥(p i.1).restr i.2.1 i.2.2 x∥ : - (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ) * ↑r ^ k : + ≤ (∑' i : Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}, + ∥(p i.1).restr i.2.1 i.2.2 x∥) * r ^ k : begin apply mul_le_mul_of_nonneg_right _ (pow_nonneg (nnreal.coe_nonneg _) _), apply norm_tsum_le_tsum_norm, @@ -779,8 +750,7 @@ variables (𝕜 f) lemma is_open_analytic_at : is_open {x | analytic_at 𝕜 f x} := begin rw is_open_iff_forall_mem_open, - assume x hx, - rcases hx with ⟨p, r, hr⟩, + rintro x ⟨p, r, hr⟩, refine ⟨emetric.ball x r, λ y hy, hr.analytic_at_of_mem hy, emetric.is_open_ball, _⟩, simp only [edist_self, emetric.mem_ball, hr.r_pos] end diff --git a/src/analysis/analytic/composition.lean b/src/analysis/analytic/composition.lean index 44c66ff7b82d9..297d7ad5e4139 100644 --- a/src/analysis/analytic/composition.lean +++ b/src/analysis/analytic/composition.lean @@ -268,13 +268,8 @@ way, as it will often appear in this form. -/ lemma id_apply_one' {n : ℕ} (h : n = 1) (v : fin n → E) : (id 𝕜 E) n v = v ⟨0, h.symm ▸ zero_lt_one⟩ := begin - let w : fin 1 → E := λ i, v ⟨i.1, h.symm ▸ i.2⟩, - have : v ⟨0, h.symm ▸ zero_lt_one⟩ = w 0 := rfl, - rw [this, ← id_apply_one 𝕜 E w], - apply congr _ h, - intros, - obtain rfl : i = 0, { linarith }, - exact this, + subst n, + apply id_apply_one end /-- For `n ≠ 1`, the `n`-th coefficient of `id 𝕜 E` is zero, by definition. -/ @@ -349,126 +344,80 @@ geometric term). -/ theorem comp_summable_nnreal (q : formal_multilinear_series 𝕜 F G) (p : formal_multilinear_series 𝕜 E F) (hq : 0 < q.radius) (hp : 0 < p.radius) : - ∃ (r : ℝ≥0), 0 < r ∧ summable (λ i, nnnorm (q.comp_along_composition p i.2) * r ^ i.1 : - (Σ n, composition n) → ℝ≥0) := + ∃ r > (0 : ℝ≥0), + summable (λ i : Σ n, composition n, nnnorm (q.comp_along_composition p i.2) * r ^ i.1) := begin /- This follows from the fact that the growth rate of `∥qₙ∥` and `∥pₙ∥` is at most geometric, giving a geometric bound on each `∥q.comp_along_composition p op∥`, together with the fact that there are `2^(n-1)` compositions of `n`, giving at most a geometric loss. -/ - rcases ennreal.lt_iff_exists_nnreal_btwn.1 hq with ⟨rq, rq_pos, hrq⟩, - rcases ennreal.lt_iff_exists_nnreal_btwn.1 hp with ⟨rp, rp_pos, hrp⟩, - obtain ⟨Cq, hCq⟩ : ∃ (Cq : ℝ≥0), ∀ n, nnnorm (q n) * rq^n ≤ Cq := q.bound_of_lt_radius hrq, - obtain ⟨Cp, hCp⟩ : ∃ (Cp : ℝ≥0), ∀ n, nnnorm (p n) * rp^n ≤ Cp := p.bound_of_lt_radius hrp, - let r0 : ℝ≥0 := (4 * max Cp 1)⁻¹, - set r := min rp 1 * min rq 1 * r0, - have r_pos : 0 < r, - { apply mul_pos (mul_pos _ _), - { rw [nnreal.inv_pos], - apply mul_pos, - { norm_num }, - { exact lt_of_lt_of_le zero_lt_one (le_max_right _ _) } }, - { rw ennreal.coe_pos at rp_pos, simp [rp_pos, zero_lt_one] }, - { rw ennreal.coe_pos at rq_pos, simp [rq_pos, zero_lt_one] } }, - let a : ennreal := ((4 : ℝ≥0) ⁻¹ : ℝ≥0), - have two_a : 2 * a < 1, - { change ((2 : ℝ≥0) : ennreal) * ((4 : ℝ≥0) ⁻¹ : ℝ≥0) < (1 : ℝ≥0), - rw [← ennreal.coe_mul, ennreal.coe_lt_coe, ← nnreal.coe_lt_coe, nnreal.coe_mul], - change (2 : ℝ) * (4 : ℝ)⁻¹ < 1, - norm_num }, + rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min ennreal.zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩, + rcases ennreal.lt_iff_exists_nnreal_btwn.1 (lt_min ennreal.zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩, + simp only [lt_min_iff, ennreal.coe_lt_one_iff, ennreal.coe_pos] at hrp hrq rp_pos rq_pos, + obtain ⟨Cq, hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, nnnorm (q n) * rq^n ≤ Cq := + q.nnnorm_mul_pow_le_of_lt_radius hrq.2, + obtain ⟨Cp, hCp1, hCp⟩ : ∃ Cp ≥ 1, ∀ n, nnnorm (p n) * rp^n ≤ Cp, + { rcases p.nnnorm_mul_pow_le_of_lt_radius hrp.2 with ⟨Cp, -, hCp⟩, + exact ⟨max Cp 1, le_max_right _ _, λ n, (hCp n).trans (le_max_left _ _)⟩ }, + let r0 : ℝ≥0 := (4 * Cp)⁻¹, + have r0_pos : 0 < r0 := nnreal.inv_pos.2 (mul_pos zero_lt_four (zero_lt_one.trans_le hCp1)), + set r : ℝ≥0 := rp * rq * r0, + have r_pos : 0 < r := mul_pos (mul_pos rp_pos rq_pos) r0_pos, have I : ∀ (i : Σ (n : ℕ), composition n), - ↑(nnnorm (q.comp_along_composition p i.2) * r ^ i.1) ≤ (Cq : ennreal) * a ^ i.1, + nnnorm (q.comp_along_composition p i.2) * r ^ i.1 ≤ Cq / 4 ^ i.1, { rintros ⟨n, c⟩, - rw [← ennreal.coe_pow, ← ennreal.coe_mul, ennreal.coe_le_coe], + have A, + calc nnnorm (q c.length) * rq ^ n ≤ nnnorm (q c.length)* rq ^ c.length : + mul_le_mul' le_rfl (pow_le_pow_of_le_one rq.2 hrq.1.le c.length_le) + ... ≤ 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 : + 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 + ... ≤ Cp ^ n : pow_le_pow hCp1 c.length_le, calc nnnorm (q.comp_along_composition p c) * r ^ n - ≤ (nnnorm (q c.length) * ∏ i, nnnorm (p (c.blocks_fun i))) * r ^ n : - mul_le_mul_of_nonneg_right (q.comp_along_composition_nnnorm p c) (bot_le) - ... = (nnnorm (q c.length) * (min rq 1)^n) * - ((∏ i, nnnorm (p (c.blocks_fun i))) * (min rp 1) ^ n) * - r0 ^ n : by { dsimp [r], ring_exp } - ... ≤ (nnnorm (q c.length) * (min rq 1) ^ c.length) * - (∏ i, nnnorm (p (c.blocks_fun i)) * (min rp 1) ^ (c.blocks_fun i)) * r0 ^ n : + ≤ (nnnorm (q c.length) * ∏ i, nnnorm (p (c.blocks_fun i))) * r ^ n : + mul_le_mul' (q.comp_along_composition_nnnorm p c) le_rfl + ... = (nnnorm (q c.length) * rq ^ n) * ((∏ i, nnnorm (p (c.blocks_fun i))) * rp ^ n) * r0 ^ n : + by { simp only [r, mul_pow], ac_refl } + ... ≤ Cq * Cp ^ n * r0 ^ n : mul_le_mul' (mul_le_mul' A B) le_rfl + ... = Cq / 4 ^ n : begin - apply_rules [mul_le_mul, bot_le, le_refl, pow_le_pow_of_le_one, min_le_right, c.length_le], - apply le_of_eq, - rw finset.prod_mul_distrib, - congr' 1, - conv_lhs { rw [← c.sum_blocks_fun, ← finset.prod_pow_eq_pow_sum] }, - end - ... ≤ Cq * (∏ i : fin c.length, Cp) * r0 ^ n : - begin - apply_rules [mul_le_mul, bot_le, le_trans _ (hCq c.length), le_refl, finset.prod_le_prod', - pow_le_pow_of_le_left, min_le_left], - assume i hi, - refine le_trans (mul_le_mul (le_refl _) _ bot_le bot_le) (hCp (c.blocks_fun i)), - exact pow_le_pow_of_le_left bot_le (min_le_left _ _) _ - end - ... ≤ Cq * (max Cp 1) ^ n * r0 ^ n : - begin - apply_rules [mul_le_mul, bot_le, le_refl], - simp only [finset.card_fin, finset.prod_const], - refine le_trans (pow_le_pow_of_le_left bot_le (le_max_left Cp 1) c.length) _, - apply pow_le_pow (le_max_right Cp 1) c.length_le, - end - ... = Cq * 4⁻¹ ^ n : - begin - dsimp [r0], - have A : (4 : ℝ≥0) ≠ 0, by norm_num, - have B : max Cp 1 ≠ 0 := - ne_of_gt (lt_of_lt_of_le zero_lt_one (le_max_right Cp 1)), - field_simp [A, B], - ring_exp + simp only [r0], + field_simp [mul_pow, (zero_lt_one.trans_le hCp1).ne'], + ac_refl end }, - refine ⟨r, r_pos, _⟩, - rw [← ennreal.tsum_coe_ne_top_iff_summable], - apply ne_of_lt, - calc (∑' (i : Σ (n : ℕ), composition n), ↑(nnnorm (q.comp_along_composition p i.2) * r ^ i.1)) - ≤ (∑' (i : Σ (n : ℕ), composition n), (Cq : ennreal) * a ^ i.1) : ennreal.tsum_le_tsum I - ... = (∑' (n : ℕ), (∑' (c : composition n), (Cq : ennreal) * a ^ n)) : ennreal.tsum_sigma' _ - ... = (∑' (n : ℕ), ↑(fintype.card (composition n)) * (Cq : ennreal) * a ^ n) : - begin - congr' 1 with n : 1, - rw [tsum_fintype, finset.sum_const, nsmul_eq_mul, finset.card_univ, mul_assoc] - end - ... ≤ (∑' (n : ℕ), (2 : ennreal) ^ n * (Cq : ennreal) * a ^ n) : - begin - apply ennreal.tsum_le_tsum (λ n, _), - apply ennreal.mul_le_mul (ennreal.mul_le_mul _ (le_refl _)) (le_refl _), - rw composition_card, - simp only [nat.cast_bit0, nat.cast_one, nat.cast_pow], - apply ennreal.pow_le_pow _ (nat.sub_le n 1), - have : (1 : ℝ≥0) ≤ (2 : ℝ≥0), by norm_num, - rw ← ennreal.coe_le_coe at this, - exact this - end - ... = (∑' (n : ℕ), (Cq : ennreal) * (2 * a) ^ n) : by { congr' 1 with n : 1, rw mul_pow, ring } - ... = (Cq : ennreal) * (1 - 2 * a) ⁻¹ : by rw [ennreal.tsum_mul_left, ennreal.tsum_geometric] - ... < ⊤ : by simp [lt_top_iff_ne_top, ennreal.mul_eq_top, two_a] + refine ⟨r, r_pos, nnreal.summable_of_le I (summable.mul_left _ _)⟩, + have h4 : ∀ n : ℕ, 0 < (4 ^ n : ℝ≥0)⁻¹ := λ n, nnreal.inv_pos.2 (pow_pos zero_lt_four _), + have : ∀ n : ℕ, has_sum (λ c : composition n, (4 ^ n : ℝ≥0)⁻¹) (2 ^ (n - 1) / 4 ^ n), + { intro n, + convert has_sum_fintype (λ c : composition n, (4 ^ n : ℝ≥0)⁻¹), + simp [finset.card_univ, composition_card, div_eq_mul_inv] }, + refine nnreal.summable_sigma.2 ⟨λ n, (this n).summable, (nnreal.summable_nat_add_iff 1).1 _⟩, + convert (nnreal.summable_geometric (nnreal.div_lt_one_of_lt one_lt_two)).mul_left (1 / 4), + ext1 n, + rw [(this _).tsum_eq, nat.add_sub_cancel], + field_simp [← mul_assoc, pow_succ', ← mul_pow, show (2 * 2 : ℝ≥0) = 4, from two_mul 2] end /-- Bounding below the radius of the composition of two formal multilinear series assuming summability over all compositions. -/ theorem le_comp_radius_of_summable (q : formal_multilinear_series 𝕜 F G) (p : formal_multilinear_series 𝕜 E F) (r : ℝ≥0) - (hr : summable (λ i, nnnorm (q.comp_along_composition p i.2) * r ^ i.1 : - (Σ n, composition n) → ℝ≥0)) : + (hr : summable (λ i : (Σ n, composition n), nnnorm (q.comp_along_composition p i.2) * r ^ i.1)) : (r : ennreal) ≤ (q.comp p).radius := begin - apply le_radius_of_bound _ (tsum (λ (i : Σ (n : ℕ), composition n), - (nnnorm (comp_along_composition q p i.snd) * r ^ i.fst))), - assume n, + refine le_radius_of_bound_nnreal _ + (∑' i : (Σ n, composition n), nnnorm (comp_along_composition q p i.snd) * r ^ i.fst) (λ n, _), calc nnnorm (formal_multilinear_series.comp q p n) * r ^ n ≤ ∑' (c : composition n), nnnorm (comp_along_composition q p c) * r ^ n : begin rw [tsum_fintype, ← finset.sum_mul], - exact mul_le_mul_of_nonneg_right (nnnorm_sum_le _ _) bot_le - end - ... ≤ ∑' (i : Σ (n : ℕ), composition n), - nnnorm (comp_along_composition q p i.snd) * r ^ i.fst : - begin - let f : composition n → (Σ (n : ℕ), composition n) := λ c, ⟨n, c⟩, - have : function.injective f, by tidy, - convert nnreal.tsum_comp_le_tsum_of_inj hr this + exact mul_le_mul' (nnnorm_sum_le _ _) le_rfl end + ... ≤ ∑' (i : Σ (n : ℕ), composition n), nnnorm (comp_along_composition q p i.snd) * r ^ i.fst : + nnreal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective end /-! @@ -649,7 +598,7 @@ begin rcases hg with ⟨rg, Hg⟩, rcases hf with ⟨rf, Hf⟩, /- The terms defining `q.comp p` are geometrically summable in a disk of some radius `r`. -/ - rcases q.comp_summable_nnreal p Hg.radius_pos Hf.radius_pos with ⟨r, r_pos, hr⟩, + rcases q.comp_summable_nnreal p Hg.radius_pos Hf.radius_pos with ⟨r, r_pos : 0 < r, hr⟩, /- We will consider `y` which is smaller than `r` and `rf`, and also small enough that `f (x + y)` is close enough to `f x` to be in the disk where `g` is well behaved. Let `min (r, rf, δ)` be this new radius.-/ diff --git a/src/analysis/analytic/radius_liminf.lean b/src/analysis/analytic/radius_liminf.lean new file mode 100644 index 0000000000000..0c64194185a74 --- /dev/null +++ b/src/analysis/analytic/radius_liminf.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2020 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Yury Kudryashov +-/ +import analysis.analytic.basic +import analysis.special_functions.pow + +/-! +# Representation of `formal_multilinear_series.radius` as a `liminf` + +In this file we prove that the radius of convergence of a `formal_multilinear_series` is equal to +$\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. This lemma can't go to `basic.lean` because this +would create a circular dependency once we redefine `exp` using `formal_multilinear_series`. +-/ +variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] +{E : Type*} [normed_group E] [normed_space 𝕜 E] +{F : Type*} [normed_group F] [normed_space 𝕜 F] + +open_locale topological_space classical big_operators nnreal +open filter asymptotics + +namespace formal_multilinear_series + +variables (p : formal_multilinear_series 𝕜 E F) + +/-- The radius of a formal multilinear series is equal to +$\liminf_{n\to\infty} \frac{1}{\sqrt[n]{∥p n∥}}$. The actual statement uses `ℝ≥0` and some +coercions. -/ +lemma radius_eq_liminf : p.radius = liminf at_top (λ n, 1/((nnnorm (p n)) ^ (1 / (n : ℝ)) : ℝ≥0)) := +begin + have : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → + ((r : ennreal) ≤ 1 / ↑(nnnorm (p n) ^ (1 / (n : ℝ))) ↔ nnnorm (p n) * r ^ n ≤ 1), + { intros r n hn, + have : 0 < (n : ℝ) := nat.cast_pos.2 hn, + conv_lhs {rw [ennreal.div_def, one_mul, ennreal.le_inv_iff_mul_le, ← ennreal.coe_mul, + ennreal.coe_le_one_iff, one_div, ← nnreal.rpow_one r, ← mul_inv_cancel this.ne', + nnreal.rpow_mul, ← nnreal.mul_rpow, ← nnreal.one_rpow (n⁻¹), + nnreal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm, nnreal.rpow_nat_cast] } }, + apply le_antisymm; refine ennreal.le_of_forall_nnreal_lt (λ r hr, _), + { rcases ((tfae_exists_lt_is_o_pow (λ n, ∥p n∥ * r ^ n) 1).out 1 7).1 (p.is_o_of_lt_radius hr) + with ⟨a, ha, H⟩, + refine le_Liminf_of_le (by apply_auto_param) (eventually_map.2 $ _), + refine H.mp ((eventually_gt_at_top 0).mono $ λ n hn₀ hn, (this _ hn₀).2 + (nnreal.coe_le_coe.1 _)), + push_cast, + exact (le_abs_self _).trans (hn.trans (pow_le_one _ ha.1.le ha.2.le)) }, + { refine p.le_radius_of_is_O (is_O.of_bound 1 _), + refine (eventually_lt_of_lt_liminf hr).mp ((eventually_gt_at_top 0).mono (λ n hn₀ hn, _)), + simpa using nnreal.coe_le_coe.2 ((this _ hn₀).1 hn.le) } +end + +end formal_multilinear_series diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index 78f26306538ac..9156c6daed573 100644 --- a/src/analysis/specific_limits.lean +++ b/src/analysis/specific_limits.lean @@ -112,7 +112,8 @@ end * 1: $f n = o(a ^ n)$ for some $0 < a < R$; * 2: $f n = O(a ^ n)$ for some $-R < a < R$; * 3: $f n = O(a ^ n)$ for some $0 < a < R$; -* 4: there exist `a < R` and a positive `C` such that $|f n| ≤ Ca^n$ for all `n`; +* 4: there exist `a < R` and `C` such that one of `C` and `R` is positive and $|f n| ≤ Ca^n$ + for all `n`; * 5: there exists `0 < a < R` and a positive `C` such that $|f n| ≤ Ca^n$ for all `n`; * 6: there exists `a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`; * 7: there exists `0 < a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`. @@ -124,7 +125,7 @@ lemma tfae_exists_lt_is_o_pow (f : ℕ → ℝ) (R : ℝ) : ∃ a ∈ Ioo 0 R, is_o f (pow a) at_top, ∃ a ∈ Ioo (-R) R, is_O f (pow a) at_top, ∃ a ∈ Ioo 0 R, is_O f (pow a) at_top, - ∃ (a < R) (C > 0), ∀ n, abs (f n) ≤ C * a ^ n, + ∃ (a < R) C (h₀ : 0 < C ∨ 0 < R), ∀ n, abs (f n) ≤ C * a ^ n, ∃ (a ∈ Ioo 0 R) (C > 0), ∀ n, abs (f n) ≤ C * a ^ n, ∃ a < R, ∀ᶠ n in at_top, abs (f n) ≤ a ^ n, ∃ a ∈ Ioo 0 R, ∀ᶠ n in at_top, abs (f n) ≤ a ^ n] := @@ -149,11 +150,13 @@ begin refine ⟨a, ha, C, hC₀, λ n, _⟩, simpa only [real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne') }, - tfae_have : 6 → 5, from λ ⟨a, ha, H⟩, ⟨a, ha.2, H⟩, + tfae_have : 6 → 5, from λ ⟨a, ha, C, H₀, H⟩, ⟨a, ha.2, C, or.inl H₀, H⟩, tfae_have : 5 → 3, - { rintro ⟨a, ha, C, hC₀, H⟩, + { rintro ⟨a, ha, C, h₀, H⟩, rcases sign_cases_of_C_mul_pow_nonneg (λ n, (abs_nonneg _).trans (H n)) with rfl | ⟨hC₀, ha₀⟩, - { exact (lt_irrefl 0 hC₀).elim }, + { obtain rfl : f = 0, by { ext n, simpa using H n }, + simp only [lt_irrefl, false_or] at h₀, + exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, is_O_zero _ _⟩ }, exact ⟨a, A ⟨ha₀, ha⟩, is_O_of_le' _ (λ n, (H n).trans $ mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le)⟩ }, -- Add 7 and 8 using 2 → 8 → 7 → 3