feat(data/real/ennreal): use notation for ennreal (#6044)

The notation for `ennreal` is `ℝ≥0∞` and it is localized to `ennreal` (though I guess it doesn't have to be?).

Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20ennreal

src/analysis/analytic/basic.lean

@@ -26,7 +26,7 @@ space is analytic, as well as the inverse on invertible operators.
 Let `p` be a formal multilinear series from `E` to `F`, i.e., `p n` is a multilinear map on `E^n`
 for `n : ℕ`.
 
-* `p.radius`: the largest `r : ennreal` such that `∥p n∥ * r^n` grows subexponentially, defined as
+* `p.radius`: the largest `r : ℝ≥0∞` such that `∥p n∥ * r^n` grows subexponentially, defined as
   a liminf.
 * `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`;
@@ -73,7 +73,7 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {F : Type*} [normed_group F] [normed_space 𝕜 F]
 {G : Type*} [normed_group G] [normed_space 𝕜 G]
 
-open_locale topological_space classical big_operators nnreal filter
+open_locale topological_space classical big_operators nnreal filter ennreal
 open set filter asymptotics
 
 /-! ### The radius of a formal multilinear series -/
@@ -84,17 +84,17 @@ 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 :=
-⨆ (r : ℝ≥0) (C : ℝ) (hr : ∀ n, ∥p n∥ * r ^ n ≤ C), (r : ennreal)
+def radius (p : formal_multilinear_series 𝕜 E F) : ℝ≥0∞ :=
+⨆ (r : ℝ≥0) (C : ℝ) (hr : ∀ n, ∥p n∥ * r ^ n ≤ C), (r : ℝ≥0∞)
 
 /-- 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)
+  (h : ∀ (n : ℕ), ∥p n∥ * r^n ≤ C) : (r : ℝ≥0∞) ≤ p.radius :=
+le_supr_of_le r $ le_supr_of_le C $ (le_supr (λ _, (r : ℝ≥0∞)) h)
 
 /-- 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 :=
+  (h : ∀ (n : ℕ), nnnorm (p n) * r^n ≤ C) : (r : ℝ≥0∞) ≤ 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`. -/
@@ -166,19 +166,19 @@ 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 :=
+  (h : (r : ℝ≥0∞) < 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 norm_le_div_pow_of_pos_of_lt_radius (p : formal_multilinear_series 𝕜 E F) {r : ℝ≥0}
-  (h0 : 0 < r) (h : (r : ennreal) < p.radius) : ∃ C > 0, ∀ n, ∥p n∥ ≤ C / r ^ n :=
+  (h0 : 0 < r) (h : (r : ℝ≥0∞) < p.radius) : ∃ C > 0, ∀ n, ∥p n∥ ≤ C / r ^ n :=
 let ⟨C, hC, hp⟩ := p.norm_mul_pow_le_of_lt_radius h in
 ⟨C, hC, λ n, iff.mpr (le_div_iff (pow_pos h0 _)) (hp n)⟩
 
 /-- 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 :=
+  (h : (r : ℝ≥0∞) < 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⟩
 
@@ -216,13 +216,13 @@ 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}
+variables {f g : E → F} {p pf pg : formal_multilinear_series 𝕜 E F} {x : E} {r r' : ℝ≥0∞}
 
 /-- 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`.
 -/
 structure has_fpower_series_on_ball
-  (f : E → F) (p : formal_multilinear_series 𝕜 E F) (x : E) (r : ennreal) : Prop :=
+  (f : E → F) (p : formal_multilinear_series 𝕜 E F) (x : E) (r : ℝ≥0∞) : Prop :=
 (r_le    : r ≤ p.radius)
 (r_pos   : 0 < r)
 (has_sum : ∀ {y}, y ∈ emetric.ball (0 : E) r → has_sum (λn:ℕ, p n (λ(i : fin n), y)) (f (x + y)))
@@ -270,7 +270,7 @@ lemma has_fpower_series_on_ball.mono
 ⟨le_trans hr hf.1, r'_pos, λ y hy, hf.has_sum (emetric.ball_subset_ball hr hy)⟩
 
 protected lemma has_fpower_series_at.eventually (hf : has_fpower_series_at f p x) :
-  ∀ᶠ r : ennreal in 𝓝[Ioi 0] 0, has_fpower_series_on_ball f p x r :=
+  ∀ᶠ r : ℝ≥0∞ in 𝓝[Ioi 0] 0, has_fpower_series_on_ball f p x r :=
 let ⟨r, hr⟩ := hf in
 mem_sets_of_superset (Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 hr.r_pos)) $
   λ r' hr', hr.mono hr'.1 hr'.2.le
@@ -344,7 +344,7 @@ sums of this power series on strict subdisks of the disk of convergence.
 This version provides an upper estimate that decreases both in `∥y∥` and `n`. See also
 `has_fpower_series_on_ball.uniform_geometric_approx` for a weaker version. -/
 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) :
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ℝ≥0∞) < r) :
   ∃ (a ∈ Ioo (0 : ℝ) 1) (C > 0), (∀ y ∈ metric.ball (0 : E) r', ∀ n,
     ∥f (x + y) - p.partial_sum n y∥ ≤ C * (a * (∥y∥ / r')) ^ n) :=
 begin
@@ -376,7 +376,7 @@ end
 /-- If a function admits a power series expansion, then it is exponentially close to the partial
 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) :
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ℝ≥0∞) < r) :
   ∃ (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
@@ -496,7 +496,7 @@ end
 partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f (x + y)`
 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) :
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ℝ≥0∞) < r) :
   tendsto_uniformly_on (λ n y, p.partial_sum n y)
     (λ y, f (x + y)) at_top (metric.ball (0 : E) r') :=
 begin
@@ -532,7 +532,7 @@ end
 partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
 is the uniform limit of `p.partial_sum n (y - x)` 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) :
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ℝ≥0∞) < r) :
   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),
@@ -575,7 +575,7 @@ lemma formal_multilinear_series.has_fpower_series_on_ball [complete_space F]
   r_pos   := h,
   has_sum := λ y hy, begin
     rw zero_add,
-    replace hy : (nnnorm y : ennreal) < p.radius,
+    replace hy : (nnnorm y : ℝ≥0∞) < p.radius,
       by { convert hy, exact (edist_eq_coe_nnnorm _).symm },
     obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, hC : 0 < C, hp⟩ :=
       p.norm_mul_pow_le_mul_pow_of_lt_radius hy,
@@ -647,7 +647,7 @@ def change_origin (x : E) : formal_multilinear_series 𝕜 E F :=
 -- Note here and below it is necessary to use `@` and provide implicit arguments using `_`,
 -- so that it is possible to use pattern matching in the lambda.
 -- Overall this seems a good trade-off in readability.
-lemma change_origin_summable_aux1 (h : (nnnorm x + r : ennreal) < p.radius) :
+lemma change_origin_summable_aux1 (h : (nnnorm x + r : ℝ≥0∞) < p.radius) :
   @summable ℝ _ _ _ ((λ ⟨n, s⟩, ∥p n∥ * ∥x∥ ^ (n - s.card) * r ^ s.card) :
     (Σ (n : ℕ), finset (fin n)) → ℝ) :=
 begin
@@ -667,7 +667,7 @@ end
 
 /-- Auxiliary lemma controlling the summability of the sequence appearing in the definition of
 `p.change_origin`, second version. -/
-lemma change_origin_summable_aux2 (h : (nnnorm x + r : ennreal) < p.radius) :
+lemma change_origin_summable_aux2 (h : (nnnorm x + r : ℝ≥0∞) < p.radius) :
   @summable ℝ _ _ _ ((λ ⟨k, n, s, hs⟩, ∥(p n).restr s hs x∥ * ↑r ^ k) :
     (Σ (k : ℕ) (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ) :=
 begin
@@ -713,11 +713,11 @@ end
 
 /-- Auxiliary lemma controlling the summability of the sequence appearing in the definition of
 `p.change_origin`, third version. -/
-lemma change_origin_summable_aux3 (k : ℕ) (h : (nnnorm x : ennreal) < p.radius) :
+lemma change_origin_summable_aux3 (k : ℕ) (h : (nnnorm x : ℝ≥0∞) < p.radius) :
   @summable ℝ _ _ _ (λ ⟨n, s, hs⟩, ∥(p n).restr s hs x∥ :
   (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ) :=
 begin
-  obtain ⟨r, rpos, hr⟩ : ∃ (r : ℝ≥0), 0 < r ∧ ((nnnorm x + r) : ennreal) < p.radius :=
+  obtain ⟨r, rpos, hr⟩ : ∃ (r : ℝ≥0), 0 < r ∧ ((nnnorm x + r) : ℝ≥0∞) < p.radius :=
     ennreal.lt_iff_exists_add_pos_lt.mp h,
   have S : @summable ℝ _ _ _ ((λ ⟨n, s, hs⟩, ∥(p n).restr s hs x∥ * (r : ℝ) ^ k) :
     (Σ (n : ℕ), {s : finset (fin n) // finset.card s = k}) → ℝ),
@@ -782,7 +782,7 @@ end
 variable [complete_space F]
 
 /-- The `k`-th coefficient of `p.change_origin` is the sum of a summable series. -/
-lemma change_origin_has_sum (k : ℕ) (h : (nnnorm x : ennreal) < p.radius) :
+lemma change_origin_has_sum (k : ℕ) (h : (nnnorm x : ℝ≥0∞) < p.radius) :
   @has_sum (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))
   (p.change_origin x k) :=
@@ -795,7 +795,7 @@ begin
 end
 
 /-- Summing the series `p.change_origin x` at a point `y` gives back `p (x + y)`-/
-theorem change_origin_eval (h : (nnnorm x + nnnorm y : ennreal) < p.radius) :
+theorem change_origin_eval (h : (nnnorm x + nnnorm y : ℝ≥0∞) < p.radius) :
   has_sum ((λk:ℕ, p.change_origin x k (λ (i : fin k), y))) (p.sum (x + y)) :=
 begin
   /- The series on the left is a series of series. If we order the terms differently, we get back
@@ -856,7 +856,7 @@ begin
   -- defining `p.change_origin`, by definition
   have J : ∀k, has_sum (λ c, A ⟨k, c⟩) (p.change_origin x k (λ(i : fin k), y)),
   { assume k,
-    have : (nnnorm x : ennreal) < radius p := lt_of_le_of_lt (le_add_right (le_refl _)) h,
+    have : (nnnorm x : ℝ≥0∞) < radius p := lt_of_le_of_lt (le_add_right (le_refl _)) h,
     convert continuous_multilinear_map.has_sum_eval (p.change_origin_has_sum k this)
       (λ(i : fin k), y),
     ext ⟨_, _, _⟩,
@@ -869,13 +869,13 @@ end formal_multilinear_series
 section
 
 variables [complete_space F] {f : E → F} {p : formal_multilinear_series 𝕜 E F} {x y : E}
-{r : ennreal}
+{r : ℝ≥0∞}
 
 /-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a
 power series on any subball of this ball (even with a different center), given by `p.change_origin`.
 -/
 theorem has_fpower_series_on_ball.change_origin
-  (hf : has_fpower_series_on_ball f p x r) (h : (nnnorm y : ennreal) < r) :
+  (hf : has_fpower_series_on_ball f p x r) (h : (nnnorm y : ℝ≥0∞) < r) :
   has_fpower_series_on_ball f (p.change_origin y) (x + y) (r - nnnorm y) :=
 { r_le := begin
     apply le_trans _ p.change_origin_radius,
@@ -884,7 +884,7 @@ theorem has_fpower_series_on_ball.change_origin
   r_pos := by simp [h],
   has_sum := begin
     assume z hz,
-    have A : (nnnorm y : ennreal) + nnnorm z < r,
+    have A : (nnnorm y : ℝ≥0∞) + nnnorm z < r,
     { have : edist z 0 < r - ↑(nnnorm y) := hz,
       rwa [edist_eq_coe_nnnorm, ennreal.lt_sub_iff_add_lt, add_comm] at this },
     convert p.change_origin_eval (lt_of_lt_of_le A hf.r_le),
@@ -899,7 +899,7 @@ lemma has_fpower_series_on_ball.analytic_at_of_mem
   (hf : has_fpower_series_on_ball f p x r) (h : y ∈ emetric.ball x r) :
   analytic_at 𝕜 f y :=
 begin
-  have : (nnnorm (y - x) : ennreal) < r, by simpa [edist_eq_coe_nnnorm_sub] using h,
+  have : (nnnorm (y - x) : ℝ≥0∞) < r, by simpa [edist_eq_coe_nnnorm_sub] using h,
   have := hf.change_origin this,
   rw [add_sub_cancel'_right] at this,
   exact this.analytic_at

src/analysis/analytic/composition.lean

@@ -72,7 +72,7 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {H : Type*} [normed_group H] [normed_space 𝕜 H]
 
 open filter list
-open_locale topological_space big_operators classical nnreal
+open_locale topological_space big_operators classical nnreal ennreal
 
 /-! ### Composing formal multilinear series -/
 
@@ -493,7 +493,7 @@ 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 : (Σ n, composition n), nnnorm (q.comp_along_composition p i.2) * r ^ i.1)) :
-  (r : ennreal) ≤ (q.comp p).radius :=
+  (r : ℝ≥0∞) ≤ (q.comp p).radius :=
 begin
   refine le_radius_of_bound_nnreal _
     (∑' i : (Σ n, composition n), nnnorm (comp_along_composition q p i.snd) * r ^ i.fst) (λ n, _),
@@ -708,7 +708,7 @@ begin
   `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.-/
   have : continuous_at f x := Hf.analytic_at.continuous_at,
-  obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ennreal) (H : 0 < δ),
+  obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ≥0∞) (H : 0 < δ),
     ∀ {z : E}, z ∈ emetric.ball x δ → f z ∈ emetric.ball (f x) rg,
   { have : emetric.ball (f x) rg ∈ 𝓝 (f x) := emetric.ball_mem_nhds _ Hg.r_pos,
     rcases emetric.mem_nhds_iff.1 (Hf.analytic_at.continuous_at this) with ⟨δ, δpos, Hδ⟩,

src/analysis/analytic/radius_liminf.lean

@@ -17,7 +17,7 @@ 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_locale topological_space classical big_operators nnreal ennreal
 open filter asymptotics
 
 namespace formal_multilinear_series
@@ -30,7 +30,7 @@ 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),
+    ((r : ℝ≥0∞) ≤ 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 [one_div, ennreal.le_inv_iff_mul_le, ← ennreal.coe_mul,

src/analysis/calculus/deriv.lean

@@ -82,7 +82,7 @@ See the explanations there.
 
 universes u v w
 noncomputable theory
-open_locale classical topological_space big_operators filter
+open_locale classical topological_space big_operators filter ennreal
 open filter asymptotics set
 open continuous_linear_map (smul_right smul_right_one_eq_iff)
 
@@ -549,7 +549,7 @@ end linear_map
 
 section analytic
 
-variables {p : formal_multilinear_series 𝕜 𝕜 F} {r : ennreal}
+variables {p : formal_multilinear_series 𝕜 𝕜 F} {r : ℝ≥0∞}
 
 protected lemma has_fpower_series_at.has_strict_deriv_at (h : has_fpower_series_at f p x) :
   has_strict_deriv_at f (p 1 (λ _, 1)) x :=

src/analysis/calculus/fderiv.lean

@@ -114,7 +114,7 @@ derivative, differentiable, Fréchet, calculus
 -/
 
 open filter asymptotics continuous_linear_map set metric
-open_locale topological_space classical nnreal asymptotics filter
+open_locale topological_space classical nnreal asymptotics filter ennreal
 
 noncomputable theory
 
@@ -913,7 +913,7 @@ end continuous_linear_map
 
 section analytic
 
-variables {p : formal_multilinear_series 𝕜 E F} {r : ennreal}
+variables {p : formal_multilinear_series 𝕜 E F} {r : ℝ≥0∞}
 
 lemma has_fpower_series_at.has_strict_fderiv_at (h : has_fpower_series_at f p x) :
   has_strict_fderiv_at f (continuous_multilinear_curry_fin1 𝕜 E F (p 1)) x :=