chore(analysis): use nnnorm notation everywhere (#13930)

This was done with a series of ad-hoc regular expressions, then cleaned up by hand.

src/analysis/analytic/composition.lean

@@ -256,7 +256,7 @@ multilinear_map.mk_continuous_norm_le _
 lemma comp_along_composition_nnnorm {n : ℕ}
   (q : formal_multilinear_series 𝕜 F G) (p : formal_multilinear_series 𝕜 E F)
   (c : composition n) :
-  nnnorm (q.comp_along_composition p c) ≤ nnnorm (q c.length) * ∏ i, nnnorm (p (c.blocks_fun i)) :=
+  ∥q.comp_along_composition p c∥₊ ≤ ∥q c.length∥₊ * ∏ i, ∥p (c.blocks_fun i)∥₊ :=
 by { rw ← nnreal.coe_le_coe, push_cast, exact q.comp_along_composition_norm p c }
 
 /-- Formal composition of two formal multilinear series. The `n`-th coefficient in the composition
@@ -432,41 +432,41 @@ 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),
-    summable (λ i : Σ n, composition n, nnnorm (q.comp_along_composition p i.2) * r ^ i.1) :=
+    summable (λ i : Σ n, composition n, ∥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 (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 :=
+  obtain ⟨Cq, hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, ∥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,
+  obtain ⟨Cp, hCp1, hCp⟩ : ∃ Cp ≥ 1, ∀ n, ∥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 / 4 ^ i.1,
+    ∥q.comp_along_composition p i.2∥₊ * r ^ i.1 ≤ Cq / 4 ^ i.1,
   { rintros ⟨n, c⟩,
     have A,
-    calc nnnorm (q c.length) * rq ^ n ≤ nnnorm (q c.length)* rq ^ c.length :
+    calc ∥q c.length∥₊ * rq ^ n ≤ ∥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 :
+    calc ((∏ i, ∥p (c.blocks_fun i)∥₊) * rp ^ n)
+        = ∏ i, ∥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 :
+    calc ∥q.comp_along_composition p c∥₊ * r ^ n
+        ≤ (∥q c.length∥₊ * ∏ i, ∥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 :
+    ... = (∥q c.length∥₊ * rq ^ n) * ((∏ i, ∥p (c.blocks_fun i)∥₊) * rp ^ n) * r0 ^ n :
           by { simp only [r, mul_pow], ring }
     ... ≤ Cq * Cp ^ n * r0 ^ n : mul_le_mul' (mul_le_mul' A B) le_rfl
     ... = Cq / 4 ^ n :
@@ -496,18 +496,18 @@ end
 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)) :
+  (hr : summable (λ i : (Σ n, composition n), ∥q.comp_along_composition p i.2∥₊ * r ^ i.1)) :
   (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, _),
-  calc nnnorm (formal_multilinear_series.comp q p n) * r ^ n ≤
-  ∑' (c : composition n), nnnorm (comp_along_composition q p c) * r ^ n :
+    (∑' i : (Σ n, composition n), ∥comp_along_composition q p i.snd∥₊ * r ^ i.fst) (λ n, _),
+  calc ∥formal_multilinear_series.comp q p n∥₊ * r ^ n ≤
+  ∑' (c : composition n), ∥comp_along_composition q p c∥₊ * r ^ n :
     begin
       rw [tsum_fintype, ← finset.sum_mul],
       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 :
+  ... ≤ ∑' (i : Σ (n : ℕ), composition n), ∥comp_along_composition q p i.snd∥₊ * r ^ i.fst :
     nnreal.tsum_comp_le_tsum_of_inj hr sigma_mk_injective
 end
 

src/analysis/analytic/radius_liminf.lean

@@ -27,10 +27,10 @@ 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)) :=
+lemma radius_eq_liminf : p.radius = liminf at_top (λ n, 1/((∥p n∥₊) ^ (1 / (n : ℝ)) : ℝ≥0)) :=
 begin
   have : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n →
-    ((r : ℝ≥0∞) ≤ 1 / ↑(nnnorm (p n) ^ (1 / (n : ℝ))) ↔ nnnorm (p n) * r ^ n ≤ 1),
+    ((r : ℝ≥0∞) ≤ 1 / ↑(∥p n∥₊ ^ (1 / (n : ℝ))) ↔ ∥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/inverse.lean

@@ -153,7 +153,7 @@ begin
 end
 
 protected lemma lipschitz (hf : approximates_linear_on f f' s c) :
-  lipschitz_with (nnnorm f' + c) (s.restrict f) :=
+  lipschitz_with (∥f'∥₊ + c) (s.restrict f) :=
 by simpa only [restrict_apply, add_sub_cancel'_right]
   using (f'.lipschitz.restrict s).add hf.lipschitz_sub
 
@@ -356,7 +356,7 @@ We also assume that either `E = {0}`, or `c < ∥f'⁻¹∥⁻¹`. We use `N` as
 
 variables {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0}
 
-local notation `N` := nnnorm (f'.symm : F →L[𝕜] E)
+local notation `N` := ∥(f'.symm : F →L[𝕜] E)∥₊
 
 protected lemma antilipschitz (hf : approximates_linear_on f (f' : E →L[𝕜] F) s c)
   (hc : subsingleton E ∨ c < N⁻¹) :
@@ -572,7 +572,7 @@ variables [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
 
 lemma approximates_deriv_on_open_nhds (hf : has_strict_fderiv_at f (f' : E →L[𝕜] F) a) :
   ∃ (s : set E) (hs : a ∈ s ∧ is_open s),
-    approximates_linear_on f (f' : E →L[𝕜] F) s ((nnnorm (f'.symm : F →L[𝕜] E))⁻¹ / 2) :=
+    approximates_linear_on f (f' : E →L[𝕜] F) s (∥(f'.symm : F →L[𝕜] E)∥₊⁻¹ / 2) :=
 begin
   refine ((nhds_basis_opens a).exists_iff _).1 _,
   exact (λ s t, approximates_linear_on.mono_set),

src/analysis/normed/group/hom.lean

@@ -47,7 +47,7 @@ def mk_normed_group_hom (f : V →+ W)
 /-- Associate to a group homomorphism a bounded group homomorphism under a norm control condition.
 
 See `add_monoid_hom.mk_normed_group_hom` for a version that uses `ℝ` for the bound. -/
-def mk_normed_group_hom' (f : V →+ W) (C : ℝ≥0) (hC : ∀ x, nnnorm (f x) ≤ C * nnnorm x) :
+def mk_normed_group_hom' (f : V →+ W) (C : ℝ≥0) (hC : ∀ x, ∥f x∥₊ ≤ C * ∥x∥₊) :
   normed_group_hom V W :=
 { bound' := ⟨C, hC⟩ .. f}
 

src/analysis/normed_space/banach.lean

@@ -52,7 +52,7 @@ end continuous_linear_map
 noncomputable def continuous_linear_equiv.to_nonlinear_right_inverse (f : E ≃L[𝕜] F) :
   continuous_linear_map.nonlinear_right_inverse (f : E →L[𝕜] F) :=
 { to_fun := f.inv_fun,
-  nnnorm := nnnorm (f.symm : F →L[𝕜] E),
+  nnnorm := ∥(f.symm : F →L[𝕜] E)∥₊,
   bound' := λ y, continuous_linear_map.le_op_norm (f.symm : F →L[𝕜] E) _,
   right_inv' := f.apply_symm_apply }
 

src/analysis/normed_space/enorm.lean

@@ -40,7 +40,7 @@ structure enorm (𝕜 : Type*) (V : Type*) [normed_field 𝕜] [add_comm_group V
 (to_fun : V → ℝ≥0∞)
 (eq_zero' : ∀ x, to_fun x = 0 → x = 0)
 (map_add_le' : ∀ x y : V, to_fun (x + y) ≤ to_fun x + to_fun y)
-(map_smul_le' : ∀ (c : 𝕜) (x : V), to_fun (c • x) ≤ nnnorm c * to_fun x)
+(map_smul_le' : ∀ (c : 𝕜) (x : V), to_fun (c • x) ≤ ∥c∥₊ * to_fun x)
 
 namespace enorm
 
@@ -61,12 +61,12 @@ lemma ext_iff {e₁ e₂ : enorm 𝕜 V} : e₁ = e₂ ↔ ∀ x, e₁ x = e₂
 @[simp, norm_cast] lemma coe_inj {e₁ e₂ : enorm 𝕜 V} : (e₁ : V → ℝ≥0∞) = e₂ ↔ e₁ = e₂ :=
 coe_fn_injective.eq_iff
 
-@[simp] lemma map_smul (c : 𝕜) (x : V) : e (c • x) = nnnorm c * e x :=
+@[simp] lemma map_smul (c : 𝕜) (x : V) : e (c • x) = ∥c∥₊ * e x :=
 le_antisymm (e.map_smul_le' c x) $
 begin
   by_cases hc : c = 0, { simp [hc] },
-  calc (nnnorm c : ℝ≥0∞) * e x = nnnorm c * e (c⁻¹ • c • x) : by rw [inv_smul_smul₀ hc]
-  ... ≤ nnnorm c * (nnnorm (c⁻¹) * e (c • x)) : _
+  calc (∥c∥₊ : ℝ≥0∞) * e x = ∥c∥₊ * e (c⁻¹ • c • x) : by rw [inv_smul_smul₀ hc]
+  ... ≤ ∥c∥₊ * (∥c⁻¹∥₊ * e (c • x)) : _
   ... = e (c • x) : _,
   { exact ennreal.mul_le_mul le_rfl (e.map_smul_le' _ _) },
   { rw [← mul_assoc, nnnorm_inv, ennreal.coe_inv,
@@ -80,8 +80,8 @@ by { rw [← zero_smul 𝕜 (0:V), e.map_smul], norm_num }
 ⟨e.eq_zero' x, λ h, h.symm ▸ e.map_zero⟩
 
 @[simp] lemma map_neg (x : V) : e (-x) = e x :=
-calc e (-x) = nnnorm (-1:𝕜) * e x : by rw [← map_smul, neg_one_smul]
-        ... = e x                 : by simp
+calc e (-x) = ∥(-1 : 𝕜)∥₊ * e x : by rw [← map_smul, neg_one_smul]
+        ... = e x               : by simp
 
 lemma map_sub_rev (x y : V) : e (x - y) = e (y - x) :=
 by rw [← neg_sub, e.map_neg]
@@ -162,7 +162,7 @@ def finite_subspace : subspace 𝕜 V :=
   zero_mem' := by simp,
   add_mem'  := λ x y hx hy, lt_of_le_of_lt (e.map_add_le x y) (ennreal.add_lt_top.2 ⟨hx, hy⟩),
   smul_mem' := λ c x (hx : _ < _),
-    calc e (c • x) = nnnorm c * e x : e.map_smul c x
+    calc e (c • x) = ∥c∥₊ * e x : e.map_smul c x
                ... < ⊤              : ennreal.mul_lt_top ennreal.coe_ne_top hx.ne }
 
 /-- Metric space structure on `e.finite_subspace`. We use `emetric_space.to_metric_space_of_dist`

src/analysis/normed_space/finite_dimension.lean

@@ -425,7 +425,7 @@ begin
       ((continuous_apply i).tendsto _).sub tendsto_const_nhds),
   simp only [sub_self, norm_zero, finset.sum_const_zero] at this,
   refine (this.eventually (gt_mem_nhds $ inv_pos.2 K0)).mono (λ g hg, _),
-  replace hg : ∑ i, nnnorm (g i - f i) < K⁻¹, by { rw ← nnreal.coe_lt_coe, push_cast, exact hg },
+  replace hg : ∑ i, ∥g i - f i∥₊ < K⁻¹, by { rw ← nnreal.coe_lt_coe, push_cast, exact hg },
   rw linear_map.ker_eq_bot,
   refine (hK.add_sub_lipschitz_with (lipschitz_with.of_dist_le_mul $ λ v u, _) hg).injective,
   simp only [dist_eq_norm, linear_map.lsum_apply, pi.sub_apply, linear_map.sum_apply,
@@ -858,7 +858,7 @@ begin
     set e := v.equiv_funL,
     have : summable (λ x, ∥e (f x)∥) := this (e.summable.2 hf),
     refine summable_of_norm_bounded _ (this.mul_left
-      ↑(nnnorm (e.symm : (fin (finrank ℝ E) → ℝ) →L[ℝ] E))) (λ i, _),
+      ↑(∥(e.symm : (fin (finrank ℝ E) → ℝ) →L[ℝ] E)∥₊)) (λ i, _),
     simpa using (e.symm : (fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_op_norm (e $ f i) },
   unfreezingI { clear_dependent E },
   -- Now we deal with `g : α → fin N → ℝ`

src/analysis/normed_space/indicator_function.lean

@@ -24,7 +24,7 @@ lemma norm_indicator_eq_indicator_norm :
 flip congr_fun a (indicator_comp_of_zero norm_zero).symm
 
 lemma nnnorm_indicator_eq_indicator_nnnorm :
-  nnnorm (indicator s f a) = indicator s (λa, nnnorm (f a)) a :=
+  ∥indicator s f a∥₊ = indicator s (λa, ∥f a∥₊) a :=
 flip congr_fun a (indicator_comp_of_zero nnnorm_zero).symm
 
 lemma norm_indicator_le_of_subset (h : s ⊆ t) (f : α → E) (a : α) :

src/analysis/normed_space/linear_isometry.lean

@@ -102,7 +102,7 @@ f.to_linear_map.map_smul c x
 
 @[simp] lemma norm_map (x : E) : ∥f x∥ = ∥x∥ := f.norm_map' x
 
-@[simp] lemma nnnorm_map (x : E) : nnnorm (f x) = nnnorm x := nnreal.eq $ f.norm_map x
+@[simp] lemma nnnorm_map (x : E) : ∥f x∥₊ = ∥x∥₊ := nnreal.eq $ f.norm_map x
 
 protected lemma isometry : isometry f :=
 f.to_linear_map.to_add_monoid_hom.isometry_of_norm f.norm_map
@@ -493,7 +493,7 @@ omit σ₂₁
 @[simp] lemma map_smul [module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) : e (c • x) = c • e x :=
 e.1.map_smul c x
 
-@[simp] lemma nnnorm_map (x : E) : nnnorm (e x) = nnnorm x := e.to_linear_isometry.nnnorm_map x
+@[simp] lemma nnnorm_map (x : E) : ∥e x∥₊ = ∥x∥₊ := e.to_linear_isometry.nnnorm_map x
 
 @[simp] lemma dist_map (x y : E) : dist (e x) (e y) = dist x y :=
 e.to_linear_isometry.dist_map x y

src/analysis/normed_space/multilinear.lean

@@ -408,10 +408,10 @@ by simpa only [fintype.card_fin]
 
 /-- The fundamental property of the operator norm of a continuous multilinear map:
 `∥f m∥` is bounded by `∥f∥` times the product of the `∥m i∥`, `nnnorm` version. -/
-theorem le_op_nnnorm : nnnorm (f m) ≤ nnnorm f * ∏ i, nnnorm (m i) :=
+theorem le_op_nnnorm : ∥f m∥₊ ≤ ∥f∥₊ * ∏ i, ∥m i∥₊ :=
 nnreal.coe_le_coe.1 $ by { push_cast, exact f.le_op_norm m }
 
-theorem le_of_op_nnnorm_le {C : ℝ≥0} (h : nnnorm f ≤ C) : nnnorm (f m) ≤ C * ∏ i, nnnorm (m i) :=
+theorem le_of_op_nnnorm_le {C : ℝ≥0} (h : ∥f∥₊ ≤ C) : ∥f m∥₊ ≤ C * ∏ i, ∥m i∥₊ :=
 (f.le_op_nnnorm m).trans $ mul_le_mul' h le_rfl
 
 lemma op_norm_prod (f : continuous_multilinear_map 𝕜 E G) (g : continuous_multilinear_map 𝕜 E G') :

src/analysis/normed_space/operator_norm.lean

@@ -1328,7 +1328,7 @@ begin
       exact hx.trans_lt (half_lt_self εpos) },
     simpa using this },
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
-  refine ⟨⟨δ⁻¹, _⟩ * nnnorm c, f.to_linear_map.antilipschitz_of_bound $ λx, _⟩,
+  refine ⟨⟨δ⁻¹, _⟩ * ∥c∥₊, f.to_linear_map.antilipschitz_of_bound $ λx, _⟩,
   exact inv_nonneg.2 (le_of_lt δ_pos),
   by_cases hx : f x = 0,
   { have : f x = f 0, by { simp [hx] },
@@ -1668,7 +1668,7 @@ section
 variables [ring_hom_isometric σ₂₁]
 
 protected lemma antilipschitz (e : E ≃SL[σ₁₂] F) :
-  antilipschitz_with (nnnorm (e.symm : F →SL[σ₂₁] E)) e :=
+  antilipschitz_with ∥(e.symm : F →SL[σ₂₁] E)∥₊ e :=
 e.symm.lipschitz.to_right_inverse e.left_inv
 
 lemma one_le_norm_mul_norm_symm [ring_hom_isometric σ₁₂] [nontrivial E] (e : E ≃SL[σ₁₂] F) :
@@ -1690,7 +1690,7 @@ lemma norm_symm_pos [ring_hom_isometric σ₁₂] [nontrivial E] (e : E ≃SL[σ
 pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)
 
 lemma nnnorm_symm_pos [ring_hom_isometric σ₁₂] [nontrivial E] (e : E ≃SL[σ₁₂] F) :
-  0 < nnnorm (e.symm : F →SL[σ₂₁] E) :=
+  0 < ∥(e.symm : F →SL[σ₂₁] E)∥₊ :=
 e.norm_symm_pos
 
 lemma subsingleton_or_norm_symm_pos [ring_hom_isometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
@@ -1702,7 +1702,7 @@ begin
 end
 
 lemma subsingleton_or_nnnorm_symm_pos [ring_hom_isometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
-  subsingleton E ∨ 0 < (nnnorm $ (e.symm : F →SL[σ₂₁] E)) :=
+  subsingleton E ∨ 0 < ∥(e.symm : F →SL[σ₂₁] E)∥₊ :=
 subsingleton_or_norm_symm_pos e
 
 variable (𝕜)

src/measure_theory/constructions/borel_space.lean

@@ -1807,26 +1807,26 @@ lemma measurable_nnnorm : measurable (nnnorm : α → ℝ≥0) :=
 continuous_nnnorm.measurable
 
 @[measurability]
-lemma measurable.nnnorm {f : β → α} (hf : measurable f) : measurable (λ a, nnnorm (f a)) :=
+lemma measurable.nnnorm {f : β → α} (hf : measurable f) : measurable (λ a, ∥f a∥₊) :=
 measurable_nnnorm.comp hf
 
 @[measurability]
 lemma ae_measurable.nnnorm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
-  ae_measurable (λ a, nnnorm (f a)) μ :=
+  ae_measurable (λ a, ∥f a∥₊) μ :=
 measurable_nnnorm.comp_ae_measurable hf
 
 @[measurability]
-lemma measurable_ennnorm : measurable (λ x : α, (nnnorm x : ℝ≥0∞)) :=
+lemma measurable_ennnorm : measurable (λ x : α, (∥x∥₊ : ℝ≥0∞)) :=
 measurable_nnnorm.coe_nnreal_ennreal
 
 @[measurability]
 lemma measurable.ennnorm {f : β → α} (hf : measurable f) :
-  measurable (λ a, (nnnorm (f a) : ℝ≥0∞)) :=
+  measurable (λ a, (∥f a∥₊ : ℝ≥0∞)) :=
 hf.nnnorm.coe_nnreal_ennreal
 
 @[measurability]
 lemma ae_measurable.ennnorm {f : β → α} {μ : measure β} (hf : ae_measurable f μ) :
-  ae_measurable (λ a, (nnnorm (f a) : ℝ≥0∞)) μ :=
+  ae_measurable (λ a, (∥f a∥₊ : ℝ≥0∞)) μ :=
 measurable_ennnorm.comp_ae_measurable hf
 
 end normed_group

src/measure_theory/constructions/prod.lean

@@ -906,14 +906,14 @@ begin
   rw [continuous_iff_continuous_at], intro g,
   refine tendsto_integral_of_L1 _ (L1.integrable_coe_fn g).integral_prod_left
     (eventually_of_forall $ λ h, (L1.integrable_coe_fn h).integral_prod_left) _,
-  simp_rw [← lintegral_fn_integral_sub (λ x, (nnnorm x : ℝ≥0∞)) (L1.integrable_coe_fn _)
+  simp_rw [← lintegral_fn_integral_sub (λ x, (∥x∥₊ : ℝ≥0∞)) (L1.integrable_coe_fn _)
     (L1.integrable_coe_fn g)],
   refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (λ i, zero_le _) _,
-  { exact λ i, ∫⁻ x, ∫⁻ y, nnnorm (i (x, y) - g (x, y)) ∂ν ∂μ },
+  { exact λ i, ∫⁻ x, ∫⁻ y, ∥i (x, y) - g (x, y)∥₊ ∂ν ∂μ },
   swap, { exact λ i, lintegral_mono (λ x, ennnorm_integral_le_lintegral_ennnorm _) },
   show tendsto (λ (i : α × β →₁[μ.prod ν] E),
-    ∫⁻ x, ∫⁻ (y : β), nnnorm (i (x, y) - g (x, y)) ∂ν ∂μ) (𝓝 g) (𝓝 0),
-  have : ∀ (i : α × β →₁[μ.prod ν] E), measurable (λ z, (nnnorm (i z - g z) : ℝ≥0∞)) :=
+    ∫⁻ x, ∫⁻ (y : β), ∥i (x, y) - g (x, y)∥₊ ∂ν ∂μ) (𝓝 g) (𝓝 0),
+  have : ∀ (i : α × β →₁[μ.prod ν] E), measurable (λ z, (∥i z - g z∥₊ : ℝ≥0∞)) :=
   λ i, ((Lp.strongly_measurable i).sub (Lp.strongly_measurable g)).ennnorm,
   simp_rw [← lintegral_prod_of_measurable _ (this _), ← L1.of_real_norm_sub_eq_lintegral,
     ← of_real_zero],

src/measure_theory/function/conditional_expectation.lean

@@ -1206,7 +1206,7 @@ begin
     of_real_integral_norm_eq_lintegral_nnnorm],
   swap, { rw [← mem_ℒp_one_iff_integrable], exact Lp.mem_ℒp _, },
   have h_eq : ∫⁻ a, ∥condexp_ind_L1_fin hm hs hμs x a∥₊ ∂μ
-    = ∫⁻ a, nnnorm (condexp_ind_smul hm hs hμs x a) ∂μ,
+    = ∫⁻ a, ∥condexp_ind_smul hm hs hμs x a∥₊ ∂μ,
   { refine lintegral_congr_ae _,
     refine (condexp_ind_L1_fin_ae_eq_condexp_ind_smul hm hs hμs x).mono (λ z hz, _),
     dsimp only,