chore(*): use notation ℝ≥0 (#5391)

Author: urkud

src/analysis/ODE/gronwall.lean

@@ -32,7 +32,7 @@ variables {E : Type*} [normed_group E] [normed_space ℝ E]
           {F : Type*} [normed_group F] [normed_space ℝ F]
 
 open metric set asymptotics filter real
-open_locale classical topological_space
+open_locale classical topological_space nnreal
 
 /-! ### Technical lemmas about `gronwall_bound` -/
 
@@ -178,7 +178,7 @@ people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in the whole space. -/
 theorem dist_le_of_approx_trajectories_ODE {v : ℝ → E → E}
-  {K : nnreal} (hv : ∀ t, lipschitz_with K (v t))
+  {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g f' g' : ℝ → E} {a b : ℝ} {εf εg δ : ℝ}
   (hf : continuous_on f (Icc a b))
   (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (f' t) (Ioi t) t)
@@ -226,7 +226,7 @@ people call this Grönwall's inequality too.
 
 This version assumes all inequalities to be true in the whole space. -/
 theorem dist_le_of_trajectories_ODE {v : ℝ → E → E}
-  {K : nnreal} (hv : ∀ t, lipschitz_with K (v t))
+  {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g : ℝ → E} {a b : ℝ} {δ : ℝ}
   (hf : continuous_on f (Icc a b))
   (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)
@@ -262,7 +262,7 @@ end
 /-- There exists only one solution of an ODE \(\dot x=v(t, x)\) with
 a given initial value provided that RHS is Lipschitz continuous in `x`. -/
 theorem ODE_solution_unique {v : ℝ → E → E}
-  {K : nnreal} (hv : ∀ t, lipschitz_with K (v t))
+  {K : ℝ≥0} (hv : ∀ t, lipschitz_with K (v t))
   {f g : ℝ → E} {a b : ℝ}
   (hf : continuous_on f (Icc a b))
   (hf' : ∀ t ∈ Ico a b, has_deriv_within_at f (v t (f t)) (Ioi t) t)

src/analysis/analytic/basic.lean

@@ -69,7 +69,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
+open_locale topological_space classical big_operators nnreal
 open filter
 
 /-! ### The radius of a formal multilinear series -/
@@ -79,22 +79,22 @@ namespace formal_multilinear_series
 /-- 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 : ℝ)) : nnreal))
+liminf at_top (λ n, 1/((nnnorm (p n)) ^ (1 / (n : ℝ)) : ℝ≥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 : nnreal) {r : nnreal}
+lemma le_radius_of_bound (p : formal_multilinear_series 𝕜 E F) (C : ℝ≥0) {r : ℝ≥0}
   (h : ∀ (n : ℕ), nnnorm (p n) * r^n ≤ C) : (r : ennreal) ≤ p.radius :=
 begin
-  have L : tendsto (λ n : ℕ, (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : nnreal))
-    at_top (𝓝 ((r : ennreal) / ((C + 1)^(0 : ℝ) : nnreal))),
+  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 : ℝ)) : nnreal) * (1 / (nnnorm (p n) ^ (1/(n:ℝ)) : nnreal)),
+    (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,
@@ -103,21 +103,21 @@ begin
     { simp },
     { simp } },
   have B : ∀ᶠ (n : ℕ) in at_top,
-    (r : ennreal) / ((C + 1)^(1/(n : ℝ)) : nnreal) ≤ 1 / (nnnorm (p n) ^ (1/(n:ℝ)) : nnreal),
+    (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 : ℝ)) : nnreal)) ≤ p.radius :=
+  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
 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 : nnreal}
-  (h : (r : ennreal) < p.radius) : ∃ (C : nnreal), ∀ n, nnnorm (p n) * r^n ≤ C :=
+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 :=
 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),
@@ -143,14 +143,14 @@ begin
 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 : nnreal}
+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 :=
 begin
-  obtain ⟨t, rt, tp⟩ : ∃ (t : nnreal), (r : ennreal) < t ∧ (t : ennreal) < p.radius :=
+  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 : nnreal), ∀ n, nnnorm (p n) * t^n ≤ C := p.bound_of_lt_radius tp,
+  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 }
@@ -163,9 +163,9 @@ lemma min_radius_le_radius_add (p q : formal_multilinear_series 𝕜 E F) :
 begin
   refine le_of_forall_ge_of_dense (λ r hr, _),
   cases r, { simpa using hr },
-  obtain ⟨Cp, hCp⟩ : ∃ (C : nnreal), ∀ n, nnnorm (p n) * r^n ≤ C :=
+  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 : nnreal), ∀ n, nnnorm (q n) * r^n ≤ C :=
+  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,
@@ -314,9 +314,9 @@ let ⟨rf, hrf⟩ := hf in hrf.coeff_zero v
 
 /-- 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' : nnreal}
+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 : nnreal), a < 1 ∧ (∀ y ∈ metric.ball (0 : E) r', ∀ n,
+  ∃ (a C : ℝ≥0), a < 1 ∧ (∀ 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 :=
@@ -344,7 +344,7 @@ end
 /-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
 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' : nnreal}
+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') :=
 begin
@@ -378,7 +378,7 @@ end
 /-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
 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' : nnreal}
+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 - x)) f at_top (metric.ball (x : E) r') :=
 begin
@@ -476,7 +476,7 @@ discussion is that the set of points where a function is analytic is open.
 
 namespace formal_multilinear_series
 
-variables (p : formal_multilinear_series 𝕜 E F) {x y : E} {r : nnreal}
+variables (p : formal_multilinear_series 𝕜 E F) {x y : E} {r : ℝ≥0}
 
 /--
 Changing the origin of a formal multilinear series `p`, so that
@@ -504,7 +504,7 @@ 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)) → nnreal :=
+  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 : ℝ)),
@@ -513,7 +513,7 @@ begin
   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) : nnreal) : ennreal)) :
+  ... ≤ (∑' 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],
@@ -582,7 +582,7 @@ lemma change_origin_summable_aux3 (k : ℕ) (h : (nnnorm x : ennreal) < 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 : nnreal), 0 < r ∧ ((nnnorm x + r) : ennreal) < p.radius :=
+  obtain ⟨r, rpos, hr⟩ : ∃ (r : ℝ≥0), 0 < r ∧ ((nnnorm x + r) : ennreal) < 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}) → ℝ),

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
+open_locale topological_space big_operators classical nnreal
 
 /-! ### Composing formal multilinear series -/
 
@@ -349,17 +349,17 @@ 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 : nnreal), 0 < r ∧ summable (λ i, nnnorm (q.comp_along_composition p i.2) * r ^ i.1 :
-    (Σ n, composition n) → nnreal) :=
+  ∃ (r : ℝ≥0), 0 < r ∧ summable (λ i, nnnorm (q.comp_along_composition p i.2) * r ^ i.1 :
+    (Σ n, composition n) → ℝ≥0) :=
 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 : nnreal), ∀ n, nnnorm (q n) * rq^n ≤ Cq := q.bound_of_lt_radius hrq,
-  obtain ⟨Cp, hCp⟩ : ∃ (Cp : nnreal), ∀ n, nnnorm (p n) * rp^n ≤ Cp := p.bound_of_lt_radius hrp,
-  let r0 : nnreal := (4 * max Cp 1)⁻¹,
+  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 _ _),
@@ -369,9 +369,9 @@ begin
       { 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 : nnreal) ⁻¹ : nnreal),
+  let a : ennreal := ((4 : ℝ≥0) ⁻¹ : ℝ≥0),
   have two_a : 2 * a < 1,
-  { change ((2 : nnreal) : ennreal) * ((4 : nnreal) ⁻¹ : nnreal) < (1 : nnreal),
+  { 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 },
@@ -412,7 +412,7 @@ begin
     ... = Cq * 4⁻¹ ^ n :
       begin
         dsimp [r0],
-        have A : (4 : nnreal) ≠ 0, by norm_num,
+        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],
@@ -436,7 +436,7 @@ begin
       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 : nnreal) ≤ (2 : nnreal), by norm_num,
+      have : (1 : ℝ≥0) ≤ (2 : ℝ≥0), by norm_num,
       rw ← ennreal.coe_le_coe at this,
       exact this
     end
@@ -448,9 +448,9 @@ 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 : nnreal)
+  (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) → nnreal)) :
+    (Σ n, composition n) → ℝ≥0)) :
   (r : ennreal) ≤ (q.comp p).radius :=
 begin
   apply le_radius_of_bound _ (tsum (λ (i : Σ (n : ℕ), composition n),

src/analysis/mean_inequalities.lean

@@ -921,11 +921,11 @@ end
 
 end ennreal
 
-/-- Hölder's inequality for functions `α → nnreal`. The integral of the product of two functions
+/-- Hölder's inequality for functions `α → ℝ≥0`. The integral of the product of two functions
 is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are conjugate
 exponents. -/
 theorem nnreal.lintegral_mul_le_Lp_mul_Lq {p q : ℝ} (hpq : p.is_conjugate_exponent q)
-  {f g : α → nnreal} (hf : measurable f) (hg : measurable g) :
+  {f g : α → ℝ≥0} (hf : measurable f) (hg : measurable g) :
   ∫⁻ a, (f * g) a ∂μ ≤ (∫⁻ a, (f a)^p ∂μ)^(1/p) * (∫⁻ a, (g a)^q ∂μ)^(1/q) :=
 begin
   simp_rw [pi.mul_apply, ennreal.coe_mul],

src/analysis/normed_space/basic.lean

@@ -299,12 +299,12 @@ finset.le_sum_of_subadditive nnnorm nnnorm_zero nnnorm_add_le
 
 end nnnorm
 
-lemma lipschitz_with.neg {α : Type*} [emetric_space α] {K : nnreal} {f : α → β}
+lemma lipschitz_with.neg {α : Type*} [emetric_space α] {K : ℝ≥0} {f : α → β}
   (hf : lipschitz_with K f) : lipschitz_with K (λ x, -f x) :=
 λ x y, by simpa only [edist_dist, dist_neg_neg] using hf x y
 
-lemma lipschitz_with.add {α : Type*} [emetric_space α] {Kf : nnreal} {f : α → β}
-  (hf : lipschitz_with Kf f) {Kg : nnreal} {g : α → β} (hg : lipschitz_with Kg g) :
+lemma lipschitz_with.add {α : Type*} [emetric_space α] {Kf : ℝ≥0} {f : α → β}
+  (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g) :
   lipschitz_with (Kf + Kg) (λ x, f x + g x) :=
 λ x y,
 calc edist (f x + g x) (f y + g y) ≤ edist (f x) (f y) + edist (g x) (g y) :
@@ -314,13 +314,13 @@ calc edist (f x + g x) (f y + g y) ≤ edist (f x) (f y) + edist (g x) (g y) :
 ... = (Kf + Kg) * edist x y :
   (add_mul _ _ _).symm
 
-lemma lipschitz_with.sub {α : Type*} [emetric_space α] {Kf : nnreal} {f : α → β}
-  (hf : lipschitz_with Kf f) {Kg : nnreal} {g : α → β} (hg : lipschitz_with Kg g) :
+lemma lipschitz_with.sub {α : Type*} [emetric_space α] {Kf : ℝ≥0} {f : α → β}
+  (hf : lipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g) :
   lipschitz_with (Kf + Kg) (λ x, f x - g x) :=
 by simpa only [sub_eq_add_neg] using hf.add hg.neg
 
-lemma antilipschitz_with.add_lipschitz_with {α : Type*} [metric_space α] {Kf : nnreal} {f : α → β}
-  (hf : antilipschitz_with Kf f) {Kg : nnreal} {g : α → β} (hg : lipschitz_with Kg g)
+lemma antilipschitz_with.add_lipschitz_with {α : Type*} [metric_space α] {Kf : ℝ≥0} {f : α → β}
+  (hf : antilipschitz_with Kf f) {Kg : ℝ≥0} {g : α → β} (hg : lipschitz_with Kg g)
   (hK : Kg < Kf⁻¹) :
   antilipschitz_with (Kf⁻¹ - Kg)⁻¹ (λ x, f x + g x) :=
 begin
@@ -365,7 +365,7 @@ max_le_iff
 /-- normed group instance on the product of finitely many normed groups, using the sup norm. -/
 instance pi.normed_group {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] :
   normed_group (Πi, π i) :=
-{ norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : nnreal) : ℝ),
+{ norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : ℝ≥0) : ℝ),
   dist_eq := assume x y,
     congr_arg (coe : ℝ≥0 → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
     show nndist (x a) (y a) = nnnorm (x a - y a), from nndist_eq_nnnorm _ _ }
@@ -431,7 +431,7 @@ lemma continuous.norm [topological_space γ] {f : γ → α} (hf : continuous f)
   continuous (λ x, ∥f x∥) :=
 continuous_norm.comp hf
 
-lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
+lemma continuous_nnnorm : continuous (nnnorm : α → ℝ≥0) :=
 continuous_subtype_mk _ continuous_norm
 
 lemma filter.tendsto.nnnorm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
@@ -1166,7 +1166,7 @@ begin
   simpa using h'
 end
 
-lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → nnreal) (hg : summable g)
+lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
   (h : ∀i, nnnorm (f i) ≤ g i) : summable f :=
 summable_of_norm_bounded (λ i, (g i : ℝ)) (nnreal.summable_coe.2 hg) (λ i, by exact_mod_cast h i)