feat: ContinuousLinearMap.pi as a continuous linear equivalence

Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean

@@ -134,4 +134,35 @@ alias postcomp_compactConvergenceCLM_apply := postcompCompactConvergenceCLM_appl
 
 end comp
 
+section Pi
+
+open scoped CompactConvergenceCLM
+
+variable [TopologicalSpace E] {ι : Type*} (F : ι → Type*)
+  [∀ i, AddCommGroup (F i)] [∀ i, Module 𝕜₁ (F i)] [∀ i, TopologicalSpace (F i)]
+  [∀ i, IsTopologicalAddGroup (F i)] [∀ i, ContinuousConstSMul 𝕜₁ (F i)]
+
+variable (𝕜₁ E) in
+/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
+`Π i, E →L_c[𝕜] F i` and `E →L_c[𝕜] Π i, F i`. -/
+def CompactConvergenceCLM.piEquivL :
+    (Π i, E →L_c[𝕜₁] F i) ≃L[𝕜₁] (E →L_c[𝕜₁] Π i, F i) where
+  toFun F := ContinuousLinearMap.pi F
+  invFun f i := (ContinuousLinearMap.proj i).comp f
+  __ := UniformConvergenceCLM.piEquivL _ _ _
+
+@[simp]
+lemma CompactConvergenceCLM.piEquivL_apply
+    (T : Π i, E →L_c[𝕜₁] F i) (e : E) (i : ι) :
+    piEquivL 𝕜₁ E F T e i = T i e :=
+  rfl
+
+@[simp]
+lemma CompactConvergenceCLM.piEquivL_symm_apply
+    (T : E →L_c[𝕜₁] Π i, F i) (e : E) (i : ι) :
+    (piEquivL 𝕜₁ E F).symm T i e = T e i :=
+  rfl
+
+end Pi
+
 end CompactSets

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

@@ -251,6 +251,24 @@ theorem continuous_of_continuous_uncurry
 
 end BoundedConvergence
 
+section Pi
+
+variable (𝕜 : Type*) [NormedField 𝕜] (E : Type*) {ι : Type*} (F : ι → Type*)
+  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+  [∀ i, AddCommGroup (F i)] [∀ i, Module 𝕜 (F i)] [∀ i, TopologicalSpace (F i)]
+  [∀ i, IsTopologicalAddGroup (F i)] [∀ i, ContinuousConstSMul 𝕜 (F i)]
+
+/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
+`Π i, E →L[𝕜] F i` and `E →L[𝕜] Π i, F i`. -/
+@[simps]
+def piEquivL :
+    (Π i, E →L[𝕜] F i) ≃L[𝕜] (E →L[𝕜] Π i, F i) where
+  toFun F := ContinuousLinearMap.pi F
+  invFun f i := (ContinuousLinearMap.proj i).comp f
+  __ := UniformConvergenceCLM.piEquivL _ _ _
+
+end Pi
+
 section BilinearMaps
 variable {R 𝕜 𝕜₂ 𝕜₃ : Type*}
 variable {E F G : Type*}

Mathlib/Topology/Algebra/Module/Spaces/PointwiseConvergenceCLM.lean

@@ -165,4 +165,29 @@ def equivWeakDual : (E →Lₚₜ[𝕜] 𝕜) ≃L[𝕜] WeakDual 𝕜 E where
     WeakDual.continuous_of_continuous_eval (fun y ↦ (evalCLM _ 𝕜 y).continuous)
   continuous_invFun := continuous_of_continuous_eval (WeakBilin.eval_continuous _)
 
+section Pi
+
+variable {ι : Type*} (F : ι → Type*)
+  [∀ i, AddCommGroup (F i)] [∀ i, Module 𝕜 (F i)] [∀ i, TopologicalSpace (F i)]
+  [∀ i, IsTopologicalAddGroup (F i)] [∀ i, ContinuousConstSMul 𝕜 (F i)]
+
+variable (𝕜 E) in
+/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
+`Π i, E →Lₚₜ[𝕜] F i` and `E →Lₚₜ[𝕜] Π i, F i`. -/
+def piEquivL :
+    (Π i, E →Lₚₜ[𝕜] F i) ≃L[𝕜] (E →Lₚₜ[𝕜] Π i, F i) where
+  toFun F := ContinuousLinearMap.pi F
+  invFun f i := (ContinuousLinearMap.proj i).comp f
+  __ := UniformConvergenceCLM.piEquivL _ _ _
+
+@[simp]
+lemma piEquivL_apply (T : Π i, E →Lₚₜ[𝕜] F i) (e : E) (i : ι) :
+    piEquivL 𝕜 E F T e i = T i e := rfl
+
+@[simp]
+lemma piEquivL_symm_apply (T : E →Lₚₜ[𝕜] Π i, F i) (e : E) (i : ι) :
+    (piEquivL 𝕜 E F).symm T i e = T e i := rfl
+
+end Pi
+
 end PointwiseConvergenceCLM

Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

@@ -503,3 +503,48 @@ alias postcomp_uniformConvergenceCLM := postcompUniformConvergenceCLM
 alias postcomp_uniformConvergenceCLM_apply := postcompUniformConvergenceCLM_apply
 
 end ContinuousLinearMap
+
+section Pi
+
+open scoped UniformConvergenceCLM
+
+variable (𝕜 : Type*) [NormedField 𝕜] {E ι : Type*} (F : ι → Type*)
+  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+  [∀ i, AddCommGroup (F i)] [∀ i, Module 𝕜 (F i)] [∀ i, TopologicalSpace (F i)]
+  [∀ i, IsTopologicalAddGroup (F i)] [∀ i, ContinuousConstSMul 𝕜 (F i)]
+
+/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
+`Π i, E →Lᵤ[𝕜, 𝔖] F i` and `E →Lᵤ[𝕜, 𝔖] Π i, F i`. -/
+def UniformConvergenceCLM.piEquivL (𝔖 : Set (Set E)) :
+    (Π i, E →Lᵤ[𝕜, 𝔖] F i) ≃L[𝕜] (E →Lᵤ[𝕜, 𝔖] Π i, F i) :=
+  letI : ∀ i, UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
+  haveI : ∀ i, IsUniformAddGroup (F i) := fun i ↦ isUniformAddGroup_of_addCommGroup
+  { toFun F := ContinuousLinearMap.pi F
+    invFun f i := (ContinuousLinearMap.proj i).comp f
+    map_add' _ _ := by ext; rfl
+    map_smul' _ _ := by ext; rfl
+    left_inv _ := by ext; rfl
+    right_inv _ := by ext; rfl
+    continuous_toFun := by
+      rw [UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous_iff]
+      rw [UniformOnFun.uniformEquivPiComm _ _ |>.isUniformEmbedding.isEmbedding.continuous_iff]
+      refine continuous_pi fun i ↦ ?_
+      exact UniformConvergenceCLM.isEmbedding_coeFn _ _ _ |>.continuous.comp (continuous_apply i)
+    continuous_invFun := by
+      apply continuous_pi (A := fun i ↦ E →Lᵤ[𝕜, 𝔖] F i) fun i ↦ ?_
+      exact (ContinuousLinearMap.proj i : (Π j, F j) →L[𝕜] F i).postcompUniformConvergenceCLM 𝔖
+        |>.continuous}
+
+@[simp]
+lemma UniformConvergenceCLM.piEquivL_apply (𝔖 : Set (Set E))
+    (T : Π i, E →Lᵤ[𝕜, 𝔖] F i) (e : E) (i : ι) :
+    piEquivL 𝕜 F 𝔖 T e i = T i e :=
+  rfl
+
+@[simp]
+lemma UniformConvergenceCLM.piEquivL_symm_apply (𝔖 : Set (Set E))
+    (T : E →Lᵤ[𝕜, 𝔖] Π i, F i) (e : E) (i : ι) :
+    (piEquivL 𝕜 F 𝔖).symm T i e = T e i :=
+  rfl
+
+end Pi