feat(analysis/normed_space/normed_group_hom): add lemmas (#7875)

From LTE.

src/analysis/normed_space/SemiNormedGroup.lean

@@ -69,7 +69,7 @@ namespace SemiNormedGroup₁
 
 instance : large_category.{u} SemiNormedGroup₁ :=
 { hom := λ X Y, { f : normed_group_hom X Y // f.norm_noninc },
-  id := λ X, ⟨normed_group_hom.id, normed_group_hom.norm_noninc.id⟩,
+  id := λ X, ⟨normed_group_hom.id X, normed_group_hom.norm_noninc.id⟩,
   comp := λ X Y Z f g, ⟨(g : normed_group_hom Y Z).comp (f : normed_group_hom X Y), g.2.comp f.2⟩, }
 
 @[ext] lemma hom_ext {M N : SemiNormedGroup₁} (f g : M ⟶ N) (w : (f : M → N) = (g : M → N)) :

src/analysis/normed_space/normed_group_hom.lean

@@ -265,6 +265,8 @@ variables {f g}
 
 /-! ### The identity normed group hom -/
 
+variable (V)
+
 /-- The identity as a continuous normed group hom. -/
 @[simps]
 def id : normed_group_hom V V :=
@@ -273,25 +275,27 @@ def id : normed_group_hom V V :=
 /-- The norm of the identity is at most `1`. It is in fact `1`, except when the norm of every
 element vanishes, where it is `0`. (Since we are working with seminorms this can happen even if the
 space is non-trivial.) It means that one can not do better than an inequality in general. -/
-lemma norm_id_le : ∥(id : normed_group_hom V V)∥ ≤ 1 :=
+lemma norm_id_le : ∥(id V : normed_group_hom V V)∥ ≤ 1 :=
 op_norm_le_bound _ zero_le_one (λx, by simp)
 
 /-- If there is an element with norm different from `0`, then the norm of the identity equals `1`.
 (Since we are working with seminorms supposing that the space is non-trivial is not enough.) -/
 lemma norm_id_of_nontrivial_seminorm (h : ∃ (x : V), ∥x∥ ≠ 0 ) :
-  ∥(id : normed_group_hom V V)∥ = 1 :=
-le_antisymm norm_id_le $ let ⟨x, hx⟩ := h in
-have _ := (id : normed_group_hom V V).ratio_le_op_norm x,
+  ∥(id V)∥ = 1 :=
+le_antisymm (norm_id_le V) $ let ⟨x, hx⟩ := h in
+have _ := (id V).ratio_le_op_norm x,
 by rwa [id_apply, div_self hx] at this
 
 /-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/
-lemma norm_id {V : Type*} [normed_group V] [nontrivial V] : ∥(id : normed_group_hom V V)∥ = 1 :=
+lemma norm_id {V : Type*} [normed_group V] [nontrivial V] : ∥(id V)∥ = 1 :=
 begin
-  refine norm_id_of_nontrivial_seminorm _,
+  refine norm_id_of_nontrivial_seminorm V _,
   obtain ⟨x, hx⟩ := exists_ne (0 : V),
   exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩,
 end
 
+lemma coe_id : ((normed_group_hom.id V) : V → V) = (_root_.id : V → V) := rfl
+
 /-! ### The negation of a normed group hom -/
 
 /-- Opposite of a normed group hom. -/
@@ -368,6 +372,14 @@ lemma norm_comp_le (g : normed_group_hom V₂ V₃) (f : normed_group_hom V₁ V
   ∥g.comp f∥ ≤ ∥g∥ * ∥f∥ :=
 mk_normed_group_hom_norm_le _ (mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _)) _
 
+lemma norm_comp_le_of_le {g : normed_group_hom V₂ V₃} {C₁ C₂ : ℝ} (hg : ∥g∥ ≤ C₂) (hf : ∥f∥ ≤ C₁) :
+  ∥g.comp f∥ ≤ C₂ * C₁ :=
+le_trans (norm_comp_le g f) $ mul_le_mul hg hf (norm_nonneg _) (le_trans (norm_nonneg _) hg)
+
+lemma norm_comp_le_of_le' {g : normed_group_hom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁)
+  (hg : ∥g∥ ≤ C₂) (hf : ∥f∥ ≤ C₁) : ∥g.comp f∥ ≤ C₃ :=
+by { rw h, exact norm_comp_le_of_le hg hf }
+
 /-- Composition of normed groups hom as an additive group morphism. -/
 def comp_hom : (normed_group_hom V₂ V₃) →+ (normed_group_hom V₁ V₂) →+ (normed_group_hom V₁ V₃) :=
 add_monoid_hom.mk' (λ g, add_monoid_hom.mk' (λ f, g.comp f)
@@ -381,6 +393,14 @@ by { ext, exact f.map_zero }
 @[simp] lemma zero_comp (f : normed_group_hom V₁ V₂) : (0 : normed_group_hom V₂ V₃).comp f = 0 :=
 by { ext, refl }
 
+lemma comp_assoc {V₄: Type* } [semi_normed_group V₄] (h : normed_group_hom V₃ V₄)
+  (g : normed_group_hom V₂ V₃) (f : normed_group_hom V₁ V₂) :
+  (h.comp g).comp f = h.comp (g.comp f) :=
+by { ext, refl }
+
+lemma coe_comp (f : normed_group_hom V₁ V₂) (g : normed_group_hom V₂ V₃) :
+  (g.comp f : V₁ → V₃) = (g : V₂ → V₃) ∘ (f : V₁ → V₂) := rfl
+
 end normed_group_hom
 
 namespace normed_group_hom
@@ -476,7 +496,7 @@ end
 lemma zero : (0 : normed_group_hom V₁ V₂).norm_noninc :=
 λ v, by simp
 
-lemma id : (id : normed_group_hom V V).norm_noninc :=
+lemma id : (id V).norm_noninc :=
 λ v, le_rfl
 
 lemma comp {g : normed_group_hom V₂ V₃} {f : normed_group_hom V₁ V₂}
@@ -500,7 +520,7 @@ lemma norm_eq_of_isometry {f : normed_group_hom V W} (hf : isometry f) (v : V) :
   ∥f v∥ = ∥v∥ :=
 f.isometry_iff_norm.mp hf v
 
-lemma isometry_id : @isometry V V _ _ (id : normed_group_hom V V) :=
+lemma isometry_id : @isometry V V _ _ (id V) :=
 isometry_id
 
 lemma isometry_comp {g : normed_group_hom V₂ V₃} {f : normed_group_hom V₁ V₂}