feat(analysis/normed_space): continuous_linear_map.prod as a `linea…

…r_isometry_equiv` (#6099)

* add lemma `continuous_linear_map.op_norm_prod`;
* add `continuous_linear_map.prodₗ` and `continuous_linear_map.prodₗᵢ`;
* add `prod.topological_semimodule`;
* drop unused `is_bounded_linear_map_prod_iso`.



Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/analysis/normed_space/bounded_linear_maps.lean

@@ -145,23 +145,6 @@ end is_bounded_linear_map
 section
 variables {ι : Type*} [decidable_eq ι] [fintype ι]
 
-/-- Taking the cartesian product of two continuous linear maps is a bounded linear operation. -/
-lemma is_bounded_linear_map_prod_iso :
-  is_bounded_linear_map 𝕜 (λ(p : (E →L[𝕜] F) × (E →L[𝕜] G)), (p.1.prod p.2 : (E →L[𝕜] (F × G)))) :=
-begin
-  refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ 1 (λp, _),
-  simp only [norm, one_mul],
-  refine continuous_linear_map.op_norm_le_bound _ (le_trans (norm_nonneg _) (le_max_left _ _)) (λu, _),
-  simp only [norm, continuous_linear_map.prod, max_le_iff],
-  split,
-  { calc ∥p.1 u∥ ≤ ∥p.1∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
-    ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
-      mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) },
-  { calc ∥p.2 u∥ ≤ ∥p.2∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
-    ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
-      mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _) }
-end
-
 /-- Taking the cartesian product of two continuous multilinear maps is a bounded linear operation. -/
 lemma is_bounded_linear_map_prod_multilinear
   {E : ι → Type*} [∀i, normed_group (E i)] [∀i, normed_space 𝕜 (E i)] :

src/analysis/normed_space/operator_norm.lean

@@ -394,6 +394,22 @@ instance to_normed_algebra [nontrivial E] : normed_algebra 𝕜 (E →L[𝕜] E)
     by {rw [norm_smul, norm_id], simp},
   .. continuous_linear_map.algebra }
 
+@[simp] lemma op_norm_prod (f : E →L[𝕜] F) (g : E →L[𝕜] G) : ∥f.prod g∥ = ∥(f, g)∥ :=
+le_antisymm
+  (op_norm_le_bound _ (norm_nonneg _) $ λ x,
+    by simpa only [prod_apply, prod.norm_def, max_mul_of_nonneg, norm_nonneg]
+      using max_le_max (le_op_norm f x) (le_op_norm g x)) $
+  max_le
+    (op_norm_le_bound _ (norm_nonneg _) $ λ x, (le_max_left _ _).trans ((f.prod g).le_op_norm x))
+    (op_norm_le_bound _ (norm_nonneg _) $ λ x, (le_max_right _ _).trans ((f.prod g).le_op_norm x))
+
+/-- `continuous_linear_map.prod` as a `linear_isometry_equiv`. -/
+def prodₗᵢ (R : Type*) [ring R] [topological_space R] [module R F] [module R G]
+  [topological_module R F] [topological_module R G]
+  [smul_comm_class 𝕜 R F] [smul_comm_class 𝕜 R G] :
+  (E →L[𝕜] F) × (E →L[𝕜] G) ≃ₗᵢ[R] (E →L[𝕜] F × G) :=
+⟨prodₗ R, λ ⟨f, g⟩, op_norm_prod f g⟩
+
 /-- A continuous linear map is automatically uniformly continuous. -/
 protected theorem uniform_continuous : uniform_continuous f :=
 f.lipschitz.uniform_continuous

src/topology/algebra/module.lean

@@ -429,8 +429,7 @@ lemma mul_apply (f g : M →L[R] M) (x : M) : (f * g) x = f (g x) := rfl
 
 /-- The cartesian product of two bounded linear maps, as a bounded linear map. -/
 protected def prod (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) : M →L[R] (M₂ × M₃) :=
-{ cont := f₁.2.prod_mk f₂.2,
-  ..f₁.to_linear_map.prod f₂.to_linear_map }
+⟨(f₁ : M →ₗ[R] M₂).prod f₂, f₁.2.prod_mk f₂.2⟩
 
 @[simp, norm_cast] lemma coe_prod (f₁ : M →L[R] M₂) (f₂ : M →L[R] M₃) :
   (f₁.prod f₂ : M →ₗ[R] M₂ × M₃) = linear_map.prod f₁ f₂ :=
@@ -440,6 +439,11 @@ rfl
   f₁.prod f₂ x = (f₁ x, f₂ x) :=
 rfl
 
+instance [topological_space R] [topological_semimodule R M] [topological_semimodule R M₂] :
+  topological_semimodule R (M × M₂) :=
+⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prod_mk
+  (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩
+
 /-- Kernel of a continuous linear map. -/
 def ker (f : M →L[R] M₂) : submodule R M := (f : M →ₗ[R] M₂).ker
 
@@ -767,16 +771,27 @@ lemma smul_apply : (c • f) x = c • (f x) := rfl
 @[simp] lemma comp_smul [linear_map.compatible_smul M₂ M₃ S R] : h.comp (c • f) = c • (h.comp f) :=
 by { ext x, exact h.map_smul_of_tower c (f x) }
 
-variable [topological_add_group M₂]
+variables [has_continuous_add M₂]
 
-instance : module S (M →L[R] M₂) :=
+instance : semimodule S (M →L[R] M₂) :=
 { smul_zero := λ _, ext $ λ _, smul_zero _,
   zero_smul := λ _, ext $ λ _, zero_smul _ _,
   one_smul  := λ _, ext $ λ _, one_smul _ _,
   mul_smul  := λ _ _ _, ext $ λ _, mul_smul _ _ _,
   add_smul  := λ _ _ _, ext $ λ _, add_smul _ _ _,
   smul_add  := λ _ _ _, ext $ λ _, smul_add _ _ _ }
 
+variables (S) [has_continuous_add M₃]
+
+/-- `continuous_linear_map.prod` as a `linear_equiv`. -/
+def prodₗ : ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] (M →L[R] M₂ × M₃) :=
+{ to_fun := λ f, f.1.prod f.2,
+  inv_fun := λ f, ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩,
+  map_add' := λ f g, rfl,
+  map_smul' := λ c f, rfl,
+  left_inv := λ f, by ext; refl,
+  right_inv := λ f, by ext; refl }
+
 end smul
 
 section smul_rightₗ