[Merged by Bors] - feat(analysis/normed_space/basic): add has_nnnorm

src/analysis/normed_space/basic.lean

@@ -29,7 +29,7 @@ class has_norm (α : Type*) := (norm : α → ℝ)
 
 export has_norm (norm)
 
-notation `∥`:1024 e:1 `∥`:1 := norm e
+notation `∥` e `∥` := norm e
 
 /-- A seminormed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥`
 defines a pseudometric space structure. -/
@@ -359,35 +359,42 @@ lemma add_monoid_hom.continuous_of_bound (f : α →+ β) (C : ℝ) (h : ∀x, 
 
 section nnnorm
 
-/-- Version of the norm taking values in nonnegative reals. -/
-def nnnorm (a : α) : ℝ≥0 := ⟨norm a, norm_nonneg a⟩
+/-- Auxiliary class, endowing a type `α` with a function `nnnorm : α → ℝ≥0`. -/
+class has_nnnorm (α : Type*) := (nnnorm : α → ℝ≥0)
 
-@[simp, norm_cast] lemma coe_nnnorm (a : α) : (nnnorm a : ℝ) = norm a := rfl
+export has_nnnorm (nnnorm)
 
-lemma nndist_eq_nnnorm (a b : α) : nndist a b = nnnorm (a - b) := nnreal.eq $ dist_eq_norm _ _
+notation `∥`e`∥₊` := nnnorm e
 
-@[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
+@[priority 100] -- see Note [lower instance priority]
+instance semi_normed_group.to_has_nnnorm : has_nnnorm α := ⟨λ a, ⟨norm a, norm_nonneg a⟩⟩
+
+@[simp, norm_cast] lemma coe_nnnorm (a : α) : (∥a∥₊ : ℝ) = norm a := rfl
+
+lemma nndist_eq_nnnorm (a b : α) : nndist a b = ∥a - b∥₊ := nnreal.eq $ dist_eq_norm _ _
+
+@[simp] lemma nnnorm_zero : ∥(0 : α)∥₊ = 0 :=
 nnreal.eq norm_zero
 
-lemma nnnorm_add_le (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
+lemma nnnorm_add_le (g h : α) : ∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊ :=
 nnreal.coe_le_coe.2 $ norm_add_le g h
 
-@[simp] lemma nnnorm_neg (g : α) : nnnorm (-g) = nnnorm g :=
+@[simp] lemma nnnorm_neg (g : α) : ∥-g∥₊ = ∥g∥₊ :=
 nnreal.eq $ norm_neg g
 
-lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h) :=
+lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊ :=
 nnreal.coe_le_coe.2 $ dist_norm_norm_le g h
 
-lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ℝ≥0∞) :=
+lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (∥x∥₊ : ℝ≥0∞) :=
 ennreal.of_real_eq_coe_nnreal _
 
-lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (nnnorm (x - y) : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm_sub (x y : β) : edist x y = (∥x - y∥₊ : ℝ≥0∞) :=
 by rw [edist_dist, dist_eq_norm, of_real_norm_eq_coe_nnnorm]
 
-lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ℝ≥0∞) :=
+lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (∥x∥₊ : ℝ≥0∞) :=
 by rw [edist_eq_coe_nnnorm_sub, _root_.sub_zero]
 
-lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑(nnnorm x) < r :=
+lemma mem_emetric_ball_0_iff {x : β} {r : ℝ≥0∞} : x ∈ emetric.ball (0 : β) r ↔ ↑∥x∥₊ < r :=
 by rw [emetric.mem_ball, edist_eq_coe_nnnorm]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : α) :
@@ -399,7 +406,7 @@ lemma edist_add_add_le (g₁ g₂ h₁ h₂ : α) :
 by { simp only [edist_nndist], norm_cast, apply nndist_add_add_le }
 
 lemma nnnorm_sum_le {β} : ∀(s : finset β) (f : β → α),
-  nnnorm (∑ a in s, f a) ≤ ∑ a in s, nnnorm (f a) :=
+  ∥∑ a in s, f a∥₊ ≤ ∑ a in s, ∥f a∥₊ :=
 finset.le_sum_of_subadditive nnnorm nnnorm_zero nnnorm_add_le
 
 end nnnorm
@@ -485,7 +492,7 @@ instance prod.semi_normed_group : semi_normed_group (α × β) :=
 
 lemma prod.semi_norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnsemi_norm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
+lemma prod.nnsemi_norm_def (x : α × β) : ∥x∥₊ = max (∥x.1∥₊) (∥x.2∥₊) :=
 by { have := x.semi_norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma semi_norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -502,10 +509,10 @@ max_le_iff
 using the sup norm. -/
 instance pi.semi_normed_group {π : ι → Type*} [fintype ι] [∀i, semi_normed_group (π i)] :
   semi_normed_group (Πi, π i) :=
-{ norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : ℝ≥0) : ℝ),
+{ norm := λf, ((finset.sup finset.univ (λ b, ∥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 _ _ }
+    show nndist (x a) (y a) = ∥x a - y a∥₊, from nndist_eq_nnnorm _ _ }
 
 /-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
 component is. -/
@@ -527,7 +534,7 @@ lemma semi_norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, semi_normed_g
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnsemi_norm_const [nonempty ι] [fintype ι] (a : α) :
-  nnnorm (λ i : ι, a) = nnnorm a :=
+  ∥(λ i : ι, a)∥₊ = ∥a∥₊ :=
 nnreal.eq $ pi_semi_norm_const a
 
 lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
@@ -577,7 +584,7 @@ lemma continuous_norm : continuous (λg:α, ∥g∥) :=
 by simpa using continuous_id.dist (continuous_const : continuous (λ g, (0:α)))
 
 @[continuity]
-lemma continuous_nnnorm : continuous (nnnorm : α → ℝ≥0) :=
+lemma continuous_nnnorm : continuous (λ (a : α), ∥a∥₊) :=
 continuous_subtype_mk _ continuous_norm
 
 lemma lipschitz_with_one_norm : lipschitz_with 1 (norm : α → ℝ) :=
@@ -586,7 +593,7 @@ by simpa only [dist_zero_left] using lipschitz_with.dist_right (0 : α)
 lemma uniform_continuous_norm : uniform_continuous (norm : α → ℝ) :=
 lipschitz_with_one_norm.uniform_continuous
 
-lemma uniform_continuous_nnnorm : uniform_continuous (nnnorm : α → ℝ≥0) :=
+lemma uniform_continuous_nnnorm : uniform_continuous (λ (a : α), ∥a∥₊) :=
 uniform_continuous_subtype_mk uniform_continuous_norm _
 
 section
@@ -597,7 +604,7 @@ lemma filter.tendsto.norm {a : α} (h : tendsto f l (𝓝 a)) : tendsto (λ x, 
 tendsto_norm.comp h
 
 lemma filter.tendsto.nnnorm (h : tendsto f l (𝓝 a)) :
-  tendsto (λ x, nnnorm (f x)) l (𝓝 (nnnorm a)) :=
+  tendsto (λ x, ∥f x∥₊) l (𝓝 (∥a∥₊)) :=
 tendsto.comp continuous_nnnorm.continuous_at h
 
 end
@@ -608,25 +615,25 @@ variables [topological_space γ] {f : γ → α} {s : set γ} {a : γ} {b : α}
 
 lemma continuous.norm (h : continuous f) : continuous (λ x, ∥f x∥) := continuous_norm.comp h
 
-lemma continuous.nnnorm (h : continuous f) : continuous (λ x, nnnorm (f x)) :=
+lemma continuous.nnnorm (h : continuous f) : continuous (λ x, ∥f x∥₊) :=
 continuous_nnnorm.comp h
 
 lemma continuous_at.norm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥) a := h.norm
 
-lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, nnnorm (f x)) a := h.nnnorm
+lemma continuous_at.nnnorm (h : continuous_at f a) : continuous_at (λ x, ∥f x∥₊) a := h.nnnorm
 
 lemma continuous_within_at.norm (h : continuous_within_at f s a) :
   continuous_within_at (λ x, ∥f x∥) s a :=
 h.norm
 
 lemma continuous_within_at.nnnorm (h : continuous_within_at f s a) :
-  continuous_within_at (λ x, nnnorm (f x)) s a :=
+  continuous_within_at (λ x, ∥f x∥₊) s a :=
 h.nnnorm
 
 lemma continuous_on.norm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥) s :=
 λ x hx, (h x hx).norm
 
-lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, nnnorm (f x)) s :=
+lemma continuous_on.nnnorm (h : continuous_on f s) : continuous_on (λ x, ∥f x∥₊) s :=
 λ x hx, (h x hx).nnnorm
 
 end
@@ -754,7 +761,7 @@ begin
   rwa dist_eq_norm
 end
 
-@[simp] lemma nnnorm_eq_zero {a : α} : nnnorm a = 0 ↔ a = 0 :=
+@[simp] lemma nnnorm_eq_zero {a : α} : ∥a∥₊ = 0 ↔ a = 0 :=
 by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
 
 /-- A subgroup of a normed group is also a normed group, with the restriction of the norm. -/
@@ -774,7 +781,7 @@ instance prod.normed_group : normed_group (α × β) := { ..prod.semi_normed_gro
 
 lemma prod.norm_def (x : α × β) : ∥x∥ = (max ∥x.1∥ ∥x.2∥) := rfl
 
-lemma prod.nnnorm_def (x : α × β) : nnnorm x = max (nnnorm x.1) (nnnorm x.2) :=
+lemma prod.nnnorm_def (x : α × β) : ∥x∥₊ = max (∥x.1∥₊) (∥x.2∥₊) :=
 by { have := x.norm_def, simp only [← coe_nnnorm] at this, exact_mod_cast this }
 
 lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
@@ -811,7 +818,7 @@ lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i
 by simpa only [← dist_zero_right] using dist_pi_const a 0
 
 @[simp] lemma pi_nnnorm_const [nonempty ι] [fintype ι] (a : α) :
-  nnnorm (λ i : ι, a) = nnnorm a :=
+  ∥(λ i : ι, a)∥₊ = ∥a∥₊ :=
 nnreal.eq $ pi_norm_const a
 
 lemma tendsto_norm_nhds_within_zero : tendsto (norm : α → ℝ) (𝓝[{0}ᶜ] 0) (𝓝[set.Ioi 0] 0) :=
@@ -867,7 +874,7 @@ export norm_one_class (norm_one)
 
 attribute [simp] norm_one
 
-@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : nnnorm (1:α) = 1 :=
+@[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : ∥(1 : α)∥₊ = 1 :=
 nnreal.eq norm_one
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1047,7 +1054,7 @@ instance to_norm_one_class : norm_one_class α :=
 ⟨mul_left_cancel' (mt norm_eq_zero.1 (@one_ne_zero α _ _)) $
   by rw [← norm_mul, mul_one, mul_one]⟩
 
-@[simp] lemma nnnorm_mul (a b : α) : nnnorm (a * b) = nnnorm a * nnnorm b :=
+@[simp] lemma nnnorm_mul (a b : α) : ∥a * b∥₊ = ∥a∥₊ * ∥b∥₊ :=
 nnreal.eq $ norm_mul a b
 
 /-- `norm` as a `monoid_hom`. -/
@@ -1060,33 +1067,33 @@ nnreal.eq $ norm_mul a b
 @[simp] lemma norm_pow (a : α) : ∀ (n : ℕ), ∥a ^ n∥ = ∥a∥ ^ n :=
 (norm_hom.to_monoid_hom : α →* ℝ).map_pow a
 
-@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : nnnorm (a ^ n) = nnnorm a ^ n :=
+@[simp] lemma nnnorm_pow (a : α) (n : ℕ) : ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_pow a n
 
 @[simp] lemma norm_prod (s : finset β) (f : β → α) :
   ∥∏ b in s, f b∥ = ∏ b in s, ∥f b∥ :=
 (norm_hom.to_monoid_hom : α →* ℝ).map_prod f s
 
 @[simp] lemma nnnorm_prod (s : finset β) (f : β → α) :
-  nnnorm (∏ b in s, f b) = ∏ b in s, nnnorm (f b) :=
+  ∥∏ b in s, f b∥₊ = ∏ b in s, ∥f b∥₊ :=
 (nnnorm_hom.to_monoid_hom : α →* ℝ≥0).map_prod f s
 
 @[simp] lemma norm_div (a b : α) : ∥a / b∥ = ∥a∥ / ∥b∥ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_div a b
 
-@[simp] lemma nnnorm_div (a b : α) : nnnorm (a / b) = nnnorm a / nnnorm b :=
+@[simp] lemma nnnorm_div (a b : α) : ∥a / b∥₊ = ∥a∥₊ / ∥b∥₊ :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_div a b
 
 @[simp] lemma norm_inv (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_inv' a
 
-@[simp] lemma nnnorm_inv (a : α) : nnnorm (a⁻¹) = (nnnorm a)⁻¹ :=
+@[simp] lemma nnnorm_inv (a : α) : ∥a⁻¹∥₊ = ∥a∥₊⁻¹ :=
 nnreal.eq $ by simp
 
 @[simp] lemma norm_fpow : ∀ (a : α) (n : ℤ), ∥a^n∥ = ∥a∥^n :=
 (norm_hom : monoid_with_zero_hom α ℝ).map_fpow
 
-@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), nnnorm (a^n) = (nnnorm a)^n :=
+@[simp] lemma nnnorm_fpow : ∀ (a : α) (n : ℤ), ∥a ^ n∥₊ = ∥a∥₊ ^ n :=
 (nnnorm_hom : monoid_with_zero_hom α ℝ≥0).map_fpow
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1167,16 +1174,16 @@ abs_of_nonneg hx
 
 @[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℝ)∥ = n := abs_of_nonneg n.cast_nonneg
 
-@[simp] lemma nnnorm_coe_nat (n : ℕ) : nnnorm (n : ℝ) = n := nnreal.eq $ by simp
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℝ)∥₊ = n := nnreal.eq $ by simp
 
-@[simp] lemma norm_two : ∥(2:ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
+@[simp] lemma norm_two : ∥(2 : ℝ)∥ = 2 := abs_of_pos (@zero_lt_two ℝ _ _)
 
-@[simp] lemma nnnorm_two : nnnorm (2:ℝ) = 2 := nnreal.eq $ by simp
+@[simp] lemma nnnorm_two : ∥(2 : ℝ)∥₊ = 2 := nnreal.eq $ by simp
 
-lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : nnnorm x = ⟨x, hx⟩ :=
+lemma nnnorm_of_nonneg {x : ℝ} (hx : 0 ≤ x) : ∥x∥₊ = ⟨x, hx⟩ :=
 nnreal.eq $ norm_of_nonneg hx
 
-lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (nnnorm x : ℝ≥0∞) = ennreal.of_real x :=
+lemma ennnorm_eq_of_real {x : ℝ} (hx : 0 ≤ x) : (∥x∥₊ : ℝ≥0∞) = ennreal.of_real x :=
 by { rw [← of_real_norm_eq_coe_nnnorm, norm_of_nonneg hx] }
 
 end real
@@ -1188,16 +1195,16 @@ open_locale nnreal
 @[simp] lemma norm_eq (x : ℝ≥0) : ∥(x : ℝ)∥ = x :=
 by rw [real.norm_eq_abs, x.abs_eq]
 
-@[simp] lemma nnnorm_eq (x : ℝ≥0) : nnnorm (x : ℝ) = x :=
+@[simp] lemma nnnorm_eq (x : ℝ≥0) : ∥(x : ℝ)∥₊ = x :=
 nnreal.eq $ real.norm_of_nonneg x.2
 
 end nnreal
 
 @[simp] lemma norm_norm [semi_normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
 real.norm_of_nonneg (norm_nonneg _)
 
-@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : nnnorm ∥a∥ = nnnorm a :=
-by simp only [nnnorm, norm_norm]
+@[simp] lemma nnnorm_norm [semi_normed_group α] (a : α) : ∥∥a∥∥₊ = ∥a∥₊ :=
+by simpa [real.nnnorm_of_nonneg (norm_nonneg a)]
 
 /-- A restatement of `metric_space.tendsto_at_top` in terms of the norm. -/
 lemma normed_group.tendsto_at_top [nonempty α] [semilattice_sup α] {β : Type*} [semi_normed_group β]
@@ -1223,7 +1230,7 @@ instance : normed_comm_ring ℤ :=
 
 @[norm_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
 
-lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = nnnorm n :=
+lemma nnreal.coe_nat_abs (n : ℤ) : (n.nat_abs : ℝ≥0) = ∥n∥₊ :=
 nnreal.eq $ calc ((n.nat_abs : ℝ≥0) : ℝ)
                = (n.nat_abs : ℤ) : by simp only [int.cast_coe_nat, nnreal.coe_nat_cast]
            ... = abs n           : by simp only [← int.abs_eq_nat_abs, int.cast_abs]
@@ -1270,11 +1277,11 @@ begin
     exact nat.abs_cast n.succ, }
 end
 
-lemma nnnorm_nsmul_le (n : ℕ) (a : α) : nnnorm (n • a) ≤ n * nnnorm a :=
+lemma nnnorm_nsmul_le (n : ℕ) (a : α) : ∥n • a∥₊ ≤ n * ∥a∥₊ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
   using norm_nsmul_le n a
 
-lemma nnnorm_gsmul_le (n : ℤ) (a : α) : nnnorm (n • a) ≤ nnnorm n * nnnorm a :=
+lemma nnnorm_gsmul_le (n : ℤ) (a : α) : ∥n • a∥₊ ≤ ∥n∥₊ * ∥a∥₊ :=
 by simpa only [←nnreal.coe_le_coe, nnreal.coe_mul] using norm_gsmul_le n a
 
 end
@@ -1334,11 +1341,11 @@ end
 lemma dist_smul [semi_normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 
-lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
+lemma nnnorm_smul [semi_normed_space α β] (s : α) (x : β) : ∥s • x∥₊ = ∥s∥₊ * ∥x∥₊ :=
 nnreal.eq $ norm_smul s x
 
 lemma nndist_smul [semi_normed_space α β] (s : α) (x y : β) :
-  nndist (s • x) (s • y) = nnnorm s * nndist x y :=
+  nndist (s • x) (s • y) = ∥s∥₊ * nndist x y :=
 nnreal.eq $ dist_smul s x y
 
 lemma norm_smul_of_nonneg [semi_normed_space ℝ β] {t : ℝ} (ht : 0 ≤ t) (x : β) :
@@ -1439,8 +1446,8 @@ instance prod.semi_normed_space : semi_normed_space α (E × F) :=
 instance pi.semi_normed_space {E : ι → Type*} [fintype ι] [∀i, semi_normed_group (E i)]
   [∀i, semi_normed_space α (E i)] : semi_normed_space α (Πi, E i) :=
 { norm_smul_le := λ a f, le_of_eq $
-    show (↑(finset.sup finset.univ (λ (b : ι), nnnorm (a • f b))) : ℝ) =
-      nnnorm a * ↑(finset.sup finset.univ (λ (b : ι), nnnorm (f b))),
+    show (↑(finset.sup finset.univ (λ (b : ι), ∥a • f b∥₊)) : ℝ) =
+      ∥a∥₊ * ↑(finset.sup finset.univ (λ (b : ι), ∥f b∥₊)),
     by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
 
 /-- A subspace of a seminormed space is also a normed space, with the restriction of the norm. -/
@@ -1756,13 +1763,13 @@ begin
 end
 
 lemma summable_of_nnnorm_bounded {f : ι → α} (g : ι → ℝ≥0) (hg : summable g)
-  (h : ∀i, nnnorm (f i) ≤ g i) : summable f :=
+  (h : ∀i, ∥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)
 
 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
 summable_of_norm_bounded _ hf (assume i, le_refl _)
 
-lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λa, nnnorm (f a))) : summable f :=
+lemma summable_of_summable_nnnorm {f : ι → α} (hf : summable (λ a, ∥f a∥₊)) : summable f :=
 summable_of_nnnorm_bounded _ hf (assume i, le_refl _)
 
 end summable

src/measure_theory/bochner_integration.lean

@@ -1321,7 +1321,7 @@ begin
   apply lintegral_congr_ae,
   filter_upwards [Lp.coe_fn_pos_part f₁, hf.coe_fn_to_L1],
   assume a h₁ h₂,
-  rw [h₁, h₂, ennreal.of_real, nnnorm],
+  rw [h₁, h₂, ennreal.of_real],
   congr' 1,
   apply nnreal.eq,
   simp [real.norm_of_nonneg, le_max_right, real.coe_to_nnreal]
@@ -1334,12 +1334,11 @@ begin
   apply lintegral_congr_ae,
   filter_upwards [Lp.coe_fn_neg_part f₁, hf.coe_fn_to_L1],
   assume a h₁ h₂,
-  rw [h₁, h₂, ennreal.of_real, nnnorm],
+  rw [h₁, h₂, ennreal.of_real],
   congr' 1,
   apply nnreal.eq,
   simp only [real.norm_of_nonneg, min_le_right, neg_nonneg, real.coe_to_nnreal', subtype.coe_mk],
-  rw ← max_neg_neg,
-  simp,
+  rw [← max_neg_neg, coe_nnnorm, neg_zero, real.norm_of_nonneg (le_max_right (-f a) 0)]
 end,
 begin
   rw [eq₁, eq₂, integral, dif_pos],