feat(analysis/normed_space): prove more lemmas, rename some old lemmas (#1733)

Renamed lemmas:

* `norm_triangle` → `norm_add_le`
* `norm_triangle_sub` → `norm_sub_le`
* `norm_triangle_sum` → `norm_sum_le`
* `norm_reverse_triangle'` → `norm_sub_norm_le`
* `norm_reverse_triangle`: deleted; was a duplicate of `abs_norm_sub_norm_le`
* `nnorm_triangle` → `nnorm_add_le`

New lemmas:

* `dist_add_left`, `dist_add_right`, `dist_neg_neg`, dist_sub_left`,
  dist_sub_right`, `dist_smul`, `dist_add_add_le`, `dist_sub_sub_le`:
  operate with distances without rewriting them as norms.

* `norm_add_le_of_le`, `dist_add_add_le_of_le`,
  `dist_sub_sub_le_of_le`, `norm_sum_le_of_le` : chain a triangle-like
  inequality with an appropriate estimates on the right hand side.

Also simplify a few proofs and fix a typo in a comment.

Author: urkud

archive/sensitivity.lean

@@ -421,7 +421,7 @@ begin
                   { dsimp only [φ],
                     erw [(f $ m+1).map_finsupp_total, (ε q).map_finsupp_total, finsupp.total_apply] ; apply_instance }
     ... ≤ (coeffs y).support.sum (λ p,
-           |(coeffs y p) * (ε q $ φ $ e p)| ) : norm_triangle_sum _ $ λ p, coeffs y p * _
+           |(coeffs y p) * (ε q $ φ $ e p)| ) : norm_sum_le _ $ λ p, coeffs y p * _
     ... = (coeffs y).support.sum (λ p, |coeffs y p| * ite (q.adjacent p) 1 0) : by simp only [abs_mul, f_matrix]
     ... = ((coeffs y).support.filter (Q.adjacent q)).sum (λ p, |coeffs y p| ) : by simp [finset.sum_filter]
     ... ≤ ((coeffs y).support.filter (Q.adjacent q)).sum (λ p, |coeffs y q| ) : finset.sum_le_sum (λ p _, H_max p)

src/analysis/asymptotics.lean

@@ -302,9 +302,8 @@ begin
   filter_upwards [hc₁, hc₂],
   intros x hx₁ hx₂,
   show ∥f₁ x + f₂ x∥ ≤ (c₁ + c₂) * ∥g x∥,
-  apply le_trans (norm_triangle _ _),
   rw add_mul,
-  exact add_le_add hx₁ hx₂
+  exact norm_add_le_of_le hx₁ hx₂
 end
 
 theorem is_o.add {f₁ f₂ : α → β} {g : α → γ} {l : filter α} (h₁ : is_o f₁ g l) (h₂ : is_o f₂ g l) :
@@ -313,8 +312,7 @@ begin
   intros c cpos,
   filter_upwards [h₁ (c / 2) (half_pos cpos), h₂ (c / 2) (half_pos cpos)],
   intros x hx₁ hx₂, dsimp at hx₁ hx₂,
-  apply le_trans (norm_triangle _ _),
-  apply le_trans (add_le_add hx₁ hx₂),
+  apply le_trans (norm_add_le_of_le hx₁ hx₂),
   rw [←mul_add, ←two_mul, ←mul_assoc, div_mul_cancel _ two_ne_zero]
 end
 

src/analysis/calculus/mean_value.lean

@@ -73,16 +73,14 @@ begin
       hs ⟨hε xε, xI⟩,
     have I : ∥f x - f k∥ ≤ D * (x-k) := calc
       ∥f x - f k∥ = ∥g (x-k) + h x∥ : by { congr' 1, simp only [h], abel }
-      ... ≤ ∥g (x-k)∥ + ∥h x∥ : norm_triangle _ _
-      ... ≤ ∥g∥ * ∥x-k∥ + (D-C) * ∥x-k∥ : add_le_add (g.le_op_norm _) Ih
+      ... ≤ ∥g∥ * ∥x-k∥ + (D-C) * ∥x-k∥ : norm_add_le_of_le (g.le_op_norm _) Ih
       ... ≤ C * ∥x-k∥ + (D-C) * ∥x-k∥ :
         add_le_add_right (mul_le_mul_of_nonneg_right (bound k k_mem_K.1) (norm_nonneg _)) _
       ... = D * ∥x-k∥ : by ring
       ... = D * (x-k) : by simp [norm, abs_of_nonneg (le_of_lt (half_pos δpos))],
     have : ∥f x - f 0∥ ≤ D * x := calc
       ∥f x - f 0∥ = ∥(f x - f k) + (f k - f 0)∥ : by { congr' 1, abel }
-      ... ≤ ∥f x - f k∥ + ∥f k - f 0∥ : norm_triangle _ _
-      ... ≤ D * (x - k) + D * k : add_le_add I (k_mem_K.2)
+      ... ≤ D * (x - k) + D * k : norm_add_le_of_le I (k_mem_K.2)
       ... = D * x : by ring,
     have xK : x ∈ K := ⟨xI, this⟩,
     have : x ≤ k := le_cSup ⟨1, λy hy, hy.1.2⟩ xK,

src/analysis/convex.lean

@@ -763,7 +763,7 @@ begin
     ... = ∥a • (x - z) + b • (y - z)∥ :
       by rw [add_smul, smul_sub, smul_sub]; simp
     ... ≤ ∥a • (x - z)∥ + ∥b • (y - z)∥ :
-      norm_triangle (a • (x - z)) (b • (y - z))
+      norm_add_le (a • (x - z)) (b • (y - z))
     ... = a * dist x z + b * dist y z :
       by simp [norm_smul, normed_group.dist_eq, real.norm_eq_abs, abs_of_nonneg ha, abs_of_nonneg hb]
 end

src/analysis/normed_space/banach.lean

@@ -72,7 +72,7 @@ begin
           ∥f x - d • y∥ = ∥f x₁ - (a + d • y) - (f x₂ - a)∥ :
             by { congr' 1, simp only [x, lin.map_sub], abel }
           ... ≤ ∥f x₁ - (a + d • y)∥ + ∥f x₂ - a∥ :
-            norm_triangle_sub
+            norm_sub_le _ _
           ... ≤ δ + δ : begin
               apply add_le_add,
               { rw [← dist_eq_norm, dist_comm], exact le_of_lt h₁ },
@@ -97,7 +97,7 @@ begin
           ∥d⁻¹ • x∥ = ∥d∥⁻¹ * ∥x₁ - x₂∥ : by rw [norm_smul, normed_field.norm_inv]
           ... ≤ ((ε / 2)⁻¹ * ∥c∥ * ∥y∥) * (n + n) : begin
               refine mul_le_mul dinv _ (norm_nonneg _) _,
-              { exact le_trans (norm_triangle_sub) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂)) },
+              { exact le_trans (norm_sub_le _ _) (add_le_add (le_of_lt hx₁) (le_of_lt hx₂)) },
               { apply mul_nonneg (mul_nonneg _ (norm_nonneg _)) (norm_nonneg _),
                 exact inv_nonneg.2 (le_of_lt (half_pos εpos)) }
             end

src/analysis/normed_space/basic.lean

@@ -83,83 +83,104 @@ lemma dist_eq_norm (g h : α) : dist g h = ∥g - h∥ :=
 normed_group.dist_eq _ _
 
 @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
-by { rw[dist_eq_norm], simp }
+by rw [dist_eq_norm, sub_zero]
 
-lemma norm_triangle (g h : α) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
-calc ∥g + h∥ = ∥g - (-h)∥             : by simp
-         ... = dist g (-h)            : by simp[dist_eq_norm]
-         ... ≤ dist g 0 + dist 0 (-h) : by apply dist_triangle
-         ... = ∥g∥ + ∥h∥               : by simp[dist_eq_norm]
+lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
+by simpa only [dist_eq_norm] using dist_comm g h
+
+@[simp] lemma norm_neg (g : α) : ∥-g∥ = ∥g∥ :=
+by simpa using norm_sub_rev 0 g
+
+@[simp] lemma dist_add_left (g h₁ h₂ : α) : dist (g + h₁) (g + h₂) = dist h₁ h₂ :=
+by simp [dist_eq_norm]
+
+@[simp] lemma dist_add_right (g₁ g₂ h : α) : dist (g₁ + h) (g₂ + h) = dist g₁ g₂ :=
+by simp [dist_eq_norm]
+
+@[simp] lemma dist_neg_neg (g h : α) : dist (-g) (-h) = dist g h :=
+by simp only [dist_eq_norm, neg_sub_neg, norm_sub_rev]
+
+@[simp] lemma dist_sub_left (g h₁ h₂ : α) : dist (g - h₁) (g - h₂) = dist h₁ h₂ :=
+by simp only [sub_eq_add_neg, dist_add_left, dist_neg_neg]
+
+@[simp] lemma dist_sub_right (g₁ g₂ h : α) : dist (g₁ - h) (g₂ - h) = dist g₁ g₂ :=
+dist_add_right _ _ _
+
+/-- Triangle inequality for the norm. -/
+lemma norm_add_le (g h : α) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
+by simpa [dist_eq_norm] using dist_triangle g 0 (-h)
+
+lemma norm_add_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
+  ∥g₁ + g₂∥ ≤ n₁ + n₂ :=
+le_trans (norm_add_le g₁ g₂) (add_le_add H₁ H₂)
+
+lemma dist_add_add_le (g₁ g₂ h₁ h₂ : α) :
+  dist (g₁ + g₂) (h₁ + h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
+by simpa only [dist_add_left, dist_add_right] using dist_triangle (g₁ + g₂) (h₁ + g₂) (h₁ + h₂)
+
+lemma dist_add_add_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
+  (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
+  dist (g₁ + g₂) (h₁ + h₂) ≤ d₁ + d₂ :=
+le_trans (dist_add_add_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
+
+lemma dist_sub_sub_le (g₁ g₂ h₁ h₂ : α) :
+  dist (g₁ - g₂) (h₁ - h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
+dist_neg_neg g₂ h₂ ▸ dist_add_add_le _ _ _ _
+
+lemma dist_sub_sub_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
+  (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
+  dist (g₁ - g₂) (h₁ - h₂) ≤ d₁ + d₂ :=
+le_trans (dist_sub_sub_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
 
 @[simp] lemma norm_nonneg (g : α) : 0 ≤ ∥g∥ :=
 by { rw[←dist_zero_right], exact dist_nonneg }
 
 lemma norm_eq_zero (g : α) : ∥g∥ = 0 ↔ g = 0 :=
 by { rw[←dist_zero_right], exact dist_eq_zero }
 
-@[simp] lemma norm_zero : ∥(0:α)∥ = 0 := (norm_eq_zero _).2 (by simp)
+@[simp] lemma norm_zero : ∥(0:α)∥ = 0 := (norm_eq_zero _).2 rfl
+
+lemma norm_sum_le {β} : ∀(s : finset β) (f : β → α), ∥s.sum f∥ ≤ s.sum (λa, ∥ f a ∥) :=
+finset.le_sum_of_subadditive norm norm_zero norm_add_le
 
-lemma norm_triangle_sum {β} : ∀(s : finset β) (f : β → α), ∥s.sum f∥ ≤ s.sum (λa, ∥ f a ∥) :=
-finset.le_sum_of_subadditive norm norm_zero norm_triangle
+lemma norm_sum_le_of_le {β} (s : finset β) {f : β → α} {n : β → ℝ} (h : ∀ b ∈ s, ∥f b∥ ≤ n b) :
+  ∥s.sum f∥ ≤ s.sum n :=
+by { haveI := classical.dec_eq β, exact le_trans (norm_sum_le s f) (finset.sum_le_sum h) }
 
 lemma norm_pos_iff (g : α) : 0 < ∥ g ∥ ↔ g ≠ 0 :=
-begin
-  split ; intro h ; rw[←dist_zero_right] at *,
-  { exact dist_pos.1 h },
-  { exact dist_pos.2 h }
-end
+dist_zero_right g ▸ dist_pos
 
 lemma norm_le_zero_iff (g : α) : ∥g∥ ≤ 0 ↔ g = 0 :=
 by { rw[←dist_zero_right], exact dist_le_zero }
 
-@[simp] lemma norm_neg (g : α) : ∥-g∥ = ∥g∥ :=
-calc ∥-g∥ = ∥0 - g∥ : by simp
-      ... = dist 0 g : (dist_eq_norm 0 g).symm
-      ... = dist g 0 : dist_comm _ _
-      ... = ∥g - 0∥ : (dist_eq_norm g 0)
-      ... = ∥g∥ : by simp
-
-lemma norm_reverse_triangle' (a b : α) : ∥a∥ - ∥b∥ ≤ ∥a - b∥ :=
-by simpa using add_le_add (norm_triangle (a - b) (b)) (le_refl (-∥b∥))
+lemma norm_sub_le (g h : α) : ∥g - h∥ ≤ ∥g∥ + ∥h∥ :=
+by simpa [dist_eq_norm] using dist_triangle g 0 h
 
-lemma norm_reverse_triangle (a b : α) : abs(∥a∥ - ∥b∥) ≤ ∥a - b∥ :=
-suffices -(∥a∥ - ∥b∥) ≤ ∥a - b∥, from abs_le_of_le_of_neg_le (norm_reverse_triangle' a b) this,
-calc -(∥a∥ - ∥b∥) = ∥b∥ - ∥a∥ : by abel
-             ... ≤ ∥b - a∥ : norm_reverse_triangle' b a
-             ... = ∥a - b∥ : by rw ← norm_neg (a - b); simp
+lemma norm_sub_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
+  ∥g₁ - g₂∥ ≤ n₁ + n₂ :=
+le_trans (norm_sub_le g₁ g₂) (add_le_add H₁ H₂)
 
-lemma norm_triangle_sub {a b : α} : ∥a - b∥ ≤ ∥a∥ + ∥b∥ :=
-by simpa only [sub_eq_add_neg, norm_neg] using norm_triangle a (-b)
+lemma dist_le_norm_add_norm (g h : α) : dist g h ≤ ∥g∥ + ∥h∥ :=
+by { rw dist_eq_norm, apply norm_sub_le }
 
 lemma abs_norm_sub_norm_le (g h : α) : abs(∥g∥ - ∥h∥) ≤ ∥g - h∥ :=
-abs_le.2 $ and.intro
-  (suffices -∥g - h∥ ≤ -(∥h∥ - ∥g∥), by simpa,
-    neg_le_neg $ sub_right_le_of_le_add $
-    calc ∥h∥ = ∥h - g + g∥ : by simp
-      ... ≤ ∥h - g∥ + ∥g∥ : norm_triangle _ _
-      ... = ∥-(g - h)∥ + ∥g∥ : by simp
-      ... = ∥g - h∥ + ∥g∥ : by { rw [norm_neg (g-h)] })
-  (sub_right_le_of_le_add $ calc ∥g∥ = ∥g - h + h∥ : by simp ... ≤ ∥g-h∥ + ∥h∥ : norm_triangle _ _)
+by simpa [dist_eq_norm] using abs_dist_sub_le g h 0
+
+lemma norm_sub_norm_le (g h : α) : ∥g∥ - ∥h∥ ≤ ∥g - h∥ :=
+le_trans (le_abs_self _) (abs_norm_sub_norm_le g h)
 
 lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ≤ ∥g - h∥ :=
 abs_norm_sub_norm_le g h
 
-lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
-by rw ←norm_neg; simp
-
 lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
 theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (𝓝 0) ↔ ∀ ε > 0, { x | ∥ f x ∥ < ε } ∈ l :=
+metric.tendsto_nhds.trans $ forall_congr $ λ ε, forall_congr $ λ εgt0,
 begin
-  rw [metric.tendsto_nhds], simp only [normed_group.dist_eq, sub_zero],
-  split,
-  { intros h ε εgt0,
-    rcases h ε εgt0 with ⟨s, ssets, hs⟩,
-    exact mem_sets_of_superset ssets hs },
-  intros h ε εgt0,
-  exact ⟨_, h ε εgt0, set.subset.refl _⟩
+  simp only [dist_zero_right],
+  exact exists_sets_subset_iff
 end
 
 section nnnorm
@@ -177,8 +198,8 @@ by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
 @[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
 nnreal.eq norm_zero
 
-lemma nnnorm_triangle (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
-by simpa [nnreal.coe_le] using norm_triangle g h
+lemma nnnorm_add_le (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
+nnreal.coe_le.2 $ norm_add_le g h
 
 @[simp] lemma nnnorm_neg (g : α) : nnnorm (-g) = nnnorm g :=
 nnreal.eq $ norm_neg g
@@ -257,7 +278,7 @@ begin
   refine ⟨metric.uniform_continuous_iff.2 $ assume ε hε, ⟨ε / 2, half_pos hε, assume a b h, _⟩⟩,
   rw [prod.dist_eq, max_lt_iff, dist_eq_norm, dist_eq_norm] at h,
   calc dist (a.1 - a.2) (b.1 - b.2) = ∥(a.1 - b.1) - (a.2 - b.2)∥  : by simp [dist_eq_norm]
-    ... ≤ ∥a.1 - b.1∥ + ∥a.2 - b.2∥ : norm_triangle_sub
+    ... ≤ ∥a.1 - b.1∥ + ∥a.2 - b.2∥ : norm_sub_le _ _
     ... < ε / 2 + ε / 2 : add_lt_add h.1 h.2
     ... = ε : add_halves _
 end
@@ -315,7 +336,7 @@ instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
     begin
       apply squeeze_zero,
       { intro, apply norm_nonneg },
-      { simp only [this], intro, apply norm_triangle },
+      { simp only [this], intro, apply norm_add_le },
       { rw ←zero_add (0 : ℝ), apply tendsto_add,
         { apply squeeze_zero,
           { intro, apply norm_nonneg },
@@ -486,6 +507,9 @@ set_option class.instance_max_depth 43
 lemma norm_smul [normed_space α β] (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
 normed_space.norm_smul s x
 
+lemma dist_smul [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 [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
 nnreal.eq $ norm_smul s x
 
@@ -499,7 +523,7 @@ begin
   rw tendsto_iff_norm_tendsto_zero,
   have ineq := λ x : γ, calc
       ∥f x • g x - s • b∥ = ∥(f x • g x - s • g x) + (s • g x - s • b)∥ : by simp[add_assoc]
-                      ... ≤ ∥f x • g x - s • g x∥ + ∥s • g x - s • b∥ : norm_triangle (f x • g x - s • g x) (s • g x - s • b)
+                      ... ≤ ∥f x • g x - s • g x∥ + ∥s • g x - s • b∥ : norm_add_le (f x • g x - s • g x) (s • g x - s • b)
                       ... ≤ ∥f x - s∥*∥g x∥ + ∥s∥*∥g x - b∥ : by { rw [←smul_sub, ←sub_smul, norm_smul, norm_smul] },
   apply squeeze_zero,
   { intro t, exact norm_nonneg _ },
@@ -614,7 +638,7 @@ summable_iff_vanishing_norm.2 $ assume ε hε,
   ⟨s, assume t ht,
     have ∥t.sum g∥ < ε := hs t ht,
     have nn : 0 ≤ t.sum g := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
-    lt_of_le_of_lt (norm_triangle_sum t f) $ lt_of_le_of_lt (finset.sum_le_sum $ assume i _, h i) $
+    lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
       by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
 
 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
@@ -625,7 +649,7 @@ have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑ i, f i)
   (continuous_norm.tendsto _).comp (has_sum_tsum $ summable_of_summable_norm hf),
 have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑ i, ∥f i∥)) :=
   has_sum_tsum hf,
-le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_triangle_sum _ _
+le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_sum_le _ _
 
 end summable
 

src/analysis/normed_space/bounded_linear_maps.lean

@@ -95,9 +95,8 @@ lemma add (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g
 let ⟨hlf, Mf, hMfp, hMf⟩ := hf in
 let ⟨hlg, Mg, hMgp, hMg⟩ := hg in
 (hlf.mk' _ + hlg.mk' _).is_linear.with_bound (Mf + Mg) $ assume x,
-  calc ∥f x + g x∥ ≤ ∥f x∥ + ∥g x∥ : norm_triangle _ _
-  ... ≤ Mf * ∥x∥ + Mg * ∥x∥        : add_le_add (hMf x) (hMg x)
-  ... ≤ (Mf + Mg) * ∥x∥            : by rw add_mul
+  calc ∥f x + g x∥ ≤ Mf * ∥x∥ + Mg * ∥x∥ : norm_add_le_of_le (hMf x) (hMg x)
+               ... ≤ (Mf + Mg) * ∥x∥     : by rw add_mul
 
 lemma sub (hf : is_bounded_linear_map 𝕜 f) (hg : is_bounded_linear_map 𝕜 g) :
   is_bounded_linear_map 𝕜 (λ e, f e - g e) := add hf (neg hg)
@@ -287,8 +286,7 @@ def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E ×
   rcases h.bound with ⟨C, Cpos, hC⟩,
   refine ⟨C * ∥p.1∥ + C * ∥p.2∥, λq, _⟩,
   calc ∥f (p.1, q.2) + f (q.1, p.2)∥
-    ≤ ∥f (p.1, q.2)∥ + ∥f (q.1, p.2)∥ : norm_triangle _ _
-  ... ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : add_le_add (hC _ _) (hC _ _)
+    ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
   ... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
       apply add_le_add,
       exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
@@ -317,8 +315,7 @@ begin
   { refine continuous_linear_map.op_norm_le_bound _
       (mul_nonneg (add_nonneg (le_of_lt Cpos) (le_of_lt Cpos)) (norm_nonneg _)) (λq, _),
     calc ∥f (p.1, q.2) + f (q.1, p.2)∥
-      ≤ ∥f (p.1, q.2)∥ + ∥f (q.1, p.2)∥ : norm_triangle _ _
-    ... ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : add_le_add (hC _ _) (hC _ _)
+      ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
     ... ≤ C * ∥p∥ * ∥q∥ + C * ∥q∥ * ∥p∥ : by apply_rules [add_le_add, mul_le_mul, norm_nonneg,
       le_of_lt Cpos, le_refl, le_max_left, le_max_right, mul_nonneg, norm_nonneg, norm_nonneg,
       norm_nonneg]

src/analysis/normed_space/operator_norm.lean

@@ -221,11 +221,10 @@ lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * 
 Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
 
 /-- The operator norm satisfies the triangle inequality. -/
-theorem op_norm_triangle : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
+theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
 Inf_le _ bounds_bdd_below
   ⟨add_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x, by { rw add_mul,
-    calc _ ≤ ∥f x∥ + ∥g x∥ : norm_triangle _ _
-    ...    ≤ _             : add_le_add (le_op_norm _ _) (le_op_norm _ _) }⟩
+    exact norm_add_le_of_le (le_op_norm _ _) (le_op_norm _ _) }⟩
 
 /-- An operator is zero iff its norm vanishes. -/
 theorem op_norm_zero_iff : ∥f∥ = 0 ↔ f = 0 :=
@@ -274,7 +273,7 @@ lemma op_norm_neg : ∥-f∥ = ∥f∥ := calc
 /-- Continuous linear maps themselves form a normed space with respect to
     the operator norm. -/
 instance to_normed_group : normed_group (E →L[𝕜] F) :=
-normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_triangle, op_norm_neg⟩
+normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_add_le, op_norm_neg⟩
 
 /- The next instance should be found automatically, but it is not.
 TODO: fix me -/

src/data/padics/padic_integers.lean

@@ -139,7 +139,7 @@ instance : normed_ring ℤ_[p] :=
 instance padic_norm_z.is_absolute_value : is_absolute_value (λ z : ℤ_[p], ∥z∥) :=
 { abv_nonneg := norm_nonneg,
   abv_eq_zero := λ ⟨_, _⟩, by simp [norm_eq_zero, padic_int.zero_def],
-  abv_add := λ ⟨_,_⟩ ⟨_, _⟩, norm_triangle _ _,
+  abv_add := λ ⟨_,_⟩ ⟨_, _⟩, norm_add_le _ _,
   abv_mul := λ _ _, by unfold norm; simp [padic_norm_z] }
 
 protected lemma padic_int.pmul_comm : ∀ z1 z2 : ℤ_[p], z1*z2 = z2*z1

src/data/padics/padic_numbers.lean

@@ -19,7 +19,7 @@ p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_p, that ℚ is e
 ## Important definitions
 
 * `padic` : the type of p-adic numbers
-* `padic_norm_e` : the rational ralued p-adic norm on ℚ_p
+* `padic_norm_e` : the rational valued p-adic norm on ℚ_p
 
 ## Notation
 
@@ -728,7 +728,7 @@ instance : normed_field ℚ_[p] :=
 instance : is_absolute_value (λ a : ℚ_[p], ∥a∥) :=
 { abv_nonneg := norm_nonneg,
   abv_eq_zero := norm_eq_zero,
-  abv_add := norm_triangle,
+  abv_add := norm_add_le,
   abv_mul := by simp [has_norm.norm, padic_norm_e.mul'] }
 
 theorem rat_dense {p : ℕ} {hp : p.prime} (q : ℚ_[p]) {ε : ℝ} (hε : ε > 0) :