[Merged by Bors] - feat(analysis/normed_space/operator_norm): generalize to seminormed space

src/analysis/analytic/linear.lean

@@ -84,7 +84,7 @@ protected theorem has_fpower_series_on_ball_bilinear (f : E →L[𝕜] F →L[
     begin
       simp only [finset.sum_range_succ, finset.sum_range_one, prod.fst_add, prod.snd_add,
         f.map_add₂],
-      dsimp, simp only [add_comm, add_left_comm, sub_self, has_sum_zero]
+      dsimp, simp only [add_comm, sub_self, has_sum_zero]
     end }
 
 protected theorem has_fpower_series_at_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :

src/analysis/normed_space/extend.lean

@@ -31,7 +31,7 @@ Alternate forms which operate on `[is_scalar_tower ℝ 𝕜 F]` instead are prov
 
 open is_R_or_C
 
-variables {𝕜 : Type*} [is_R_or_C 𝕜] {F : Type*} [normed_group F] [normed_space 𝕜 F]
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {F : Type*} [semi_normed_group F] [semi_normed_space 𝕜 F]
 local notation `abs𝕜` := @is_R_or_C.abs 𝕜 _
 
 /-- Extend `fr : F →ₗ[ℝ] ℝ` to `F →ₗ[𝕜] 𝕜` in a way that will also be continuous and have its norm
@@ -78,7 +78,7 @@ lemma linear_map.extend_to_𝕜'_apply [semimodule ℝ F] [is_scalar_tower ℝ 
   fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
 
 /-- The norm of the extension is bounded by `∥fr∥`. -/
-lemma norm_bound [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) :
+lemma norm_bound [semi_normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) :
   ∥(fr.to_linear_map.extend_to_𝕜' x : 𝕜)∥ ≤ ∥fr∥ * ∥x∥ :=
 begin
   let lm : F →ₗ[𝕜] 𝕜 := fr.to_linear_map.extend_to_𝕜',
@@ -119,12 +119,12 @@ begin
 end
 
 /-- Extend `fr : F →L[ℝ] ℝ` to `F →L[𝕜] 𝕜`. -/
-noncomputable def continuous_linear_map.extend_to_𝕜' [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
+noncomputable def continuous_linear_map.extend_to_𝕜' [semi_normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
   (fr : F →L[ℝ] ℝ) :
   F →L[𝕜] 𝕜 :=
-fr.to_linear_map.extend_to_𝕜'.mk_continuous (∥fr∥) (norm_bound _)
+linear_map.mk_continuous _ (∥fr∥) (norm_bound _)
 
-lemma continuous_linear_map.extend_to_𝕜'_apply [normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
+lemma continuous_linear_map.extend_to_𝕜'_apply [semi_normed_space ℝ F] [is_scalar_tower ℝ 𝕜 F]
   (fr : F →L[ℝ] ℝ) (x : F) :
   fr.extend_to_𝕜' x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
 

src/analysis/normed_space/finite_dimension.lean

@@ -137,7 +137,7 @@ begin
     have C0_le : ∀i, C0 i ≤ C :=
       λi, finset.single_le_sum (λj hj, (hC0 j).1) (finset.mem_univ _),
     apply linear_map.continuous_of_bound _ C (λx, _),
-    rw pi_norm_le_iff,
+    rw pi_semi_norm_le_iff,
     { exact λi, le_trans ((hC0 i).2 x) (mul_le_mul_of_nonneg_right (C0_le i) (norm_nonneg _)) },
     { exact mul_nonneg C_nonneg (norm_nonneg _) } }
 end