feat: flip arguments for continuous linear maps under finite dimension assumptions

Mathlib.lean

@@ -7346,6 +7346,7 @@ public import Mathlib.Topology.Algebra.Module.Simple
 public import Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
 public import Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
+public import Mathlib.Topology.Algebra.Module.Spaces.FiniteDimensionCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
 public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -409,14 +409,21 @@ theorem TotallyBounded.isVonNBounded {s : Set E} (hs : TotallyBounded s) :
     have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
       h'' <| mk_mem_prod hz1 hz2
     refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
-    -- TODO: with dot notation, Lean timeouts on the next line. Why?
-    exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
+    exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self
   else
     haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
     exact Bornology.IsVonNBounded.of_boundedSpace
 
 end IsUniformAddGroup
 
+variable (𝕜) in
+theorem IsCompact.isVonNBounded [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
+    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E}
+    (hs : IsCompact s) : Bornology.IsVonNBounded 𝕜 s :=
+  letI := IsTopologicalAddGroup.rightUniformSpace E
+  haveI := isUniformAddGroup_of_addCommGroup (G := E)
+  hs.totallyBounded.isVonNBounded 𝕜
+
 variable (𝕜) in
 theorem Filter.Tendsto.isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
     [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]

Mathlib/Analysis/LocallyConvex/Montel.lean

@@ -78,7 +78,7 @@ end Normed
 variable {𝕜₁ 𝕜₂ : Type*} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
 variable {E F : Type*}
   [AddCommGroup E] [Module 𝕜₁ E]
-  [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜₁ E]
+  [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E]
   [AddCommGroup F] [Module 𝕜₂ F]
   [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F]
 
@@ -110,7 +110,7 @@ def _root_.ContinuousLinearEquiv.toCompactConvergenceCLM [T1Space E] [MontelSpac
     apply hs.mono
     apply UniformConvergenceCLM.topologicalSpace_mono
     intro x hx
-    exact hx.totallyBounded.isVonNBounded 𝕜₁
+    exact hx.isVonNBounded 𝕜₁
   continuous_invFun := by
     apply continuous_of_continuousAt_zero (LinearEquiv.toCompactConvergenceCLM σ E F).symm
     rw [ContinuousAt, _root_.map_zero, CompactConvergenceCLM.hasBasis_nhds_zero.tendsto_iff

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -536,35 +536,6 @@ def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
       rw [norm_smul, mul_comm]
       gcongr <;> apply norm_le_pi_norm }
 
-/-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications
-are. -/
-theorem continuousWithinAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {s : Set X} {x : X} :
-    ContinuousWithinAt f s x ↔ ∀ y, ContinuousWithinAt (fun q ↦ f q y) s x := by
-  refine ⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun h ↦ ?_⟩
-  let e : (E →L[𝕜] F) ≃L[𝕜] Fin (finrank 𝕜 E) → F :=
-    ((ContinuousLinearEquiv.ofFinrankEq (finrank_fin_fun 𝕜).symm).arrowCongr
-      (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing _)
-  rw [e.toHomeomorph.isInducing.continuousWithinAt_iff]
-  exact continuousWithinAt_pi.mpr fun i ↦ h _
-
-/-- A family of continuous linear maps is continuous on `s` iff all its applications are. -/
-theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {s : Set X} :
-    ContinuousOn f s ↔ ∀ y, ContinuousOn (fun x ↦ f x y) s := by
-  simp_rw [ContinuousOn, continuousWithinAt_clm_apply, imp_forall_iff]
-  exact forall_comm
-
-/-- A family of continuous linear maps is continuous at a point iff all its applications are. -/
-theorem continuousAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} {x : X} :
-    ContinuousAt f x ↔ ∀ y, ContinuousAt (fun q ↦ f q y) x := by
-  simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_apply]
-
-theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
-    {f : X → E →L[𝕜] F} : Continuous f ↔ ∀ y, Continuous (f · y) := by
-  simp_rw [← continuousOn_univ, continuousOn_clm_apply]
-
 end CompleteField
 
 section LocallyCompactField

Mathlib/Analysis/Normed/Operator/Compact.lean

@@ -355,18 +355,16 @@ variable {𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁] [Nontrivial
 @[continuity]
 theorem IsCompactOperator.continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : IsCompactOperator f) :
     Continuous f := by
-  letI : UniformSpace M₂ := IsTopologicalAddGroup.rightUniformSpace _
-  haveI : IsUniformAddGroup M₂ := isUniformAddGroup_of_addCommGroup
   -- Since `f` is linear, we only need to show that it is continuous at zero.
   -- Let `U` be a neighborhood of `0` in `M₂`.
   refine continuous_of_continuousAt_zero f fun U hU => ?_
   rw [map_zero] at hU
   -- The compactness of `f` gives us a compact set `K : Set M₂` such that `f ⁻¹' K` is a
   -- neighborhood of `0` in `M₁`.
   rcases hf with ⟨K, hK, hKf⟩
-  -- But any compact set is totally bounded, hence Von-Neumann bounded. Thus, `K` absorbs `U`.
+  -- But any compact set Von-Neumann bounded. Thus, `K` absorbs `U`.
   -- This gives `r > 0` such that `∀ a : 𝕜₂, r ≤ ‖a‖ → K ⊆ a • U`.
-  rcases (hK.totallyBounded.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩
+  rcases (hK.isVonNBounded 𝕜₂ hU).exists_pos with ⟨r, hr, hrU⟩
   -- Choose `c : 𝕜₂` with `r < ‖c‖`.
   rcases NormedField.exists_lt_norm 𝕜₁ r with ⟨c, hc⟩
   have hcnz : c ≠ 0 := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm

Mathlib/Topology/Algebra/Module/Equiv.lean

@@ -708,6 +708,17 @@ def arrowCongrEquiv (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[
     ContinuousLinearMap.ext fun x => by
       simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]
 
+/-- A pair of continuous (semi)linear equivalences generates a linear equivalence between the spaces
+of continuous linear maps. See also `ContinuousLinearEquiv.arrowCongr`. -/
+@[simps]
+def arrowCongrEquivₛₗ [SMulCommClass R₃ R₃ M₃] [SMulCommClass R₄ R₄ M₄]
+    [ContinuousAdd M₃] [ContinuousConstSMul R₃ M₃] [ContinuousAdd M₄] [ContinuousConstSMul R₄ M₄]
+    (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) :
+    (M₁ →SL[σ₁₄] M₄) ≃ₛₗ[σ₄₃] (M₂ →SL[σ₂₃] M₃) where
+  toEquiv := arrowCongrEquiv e₁₂ e₄₃
+  map_add' := by simp
+  map_smul' := by simp
+
 section Pi
 
 /-- Combine a family of linear equivalences into a linear equivalence of `pi`-types.

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

@@ -65,11 +65,11 @@ notation:25 E " →L_c[" R "] " F => CompactConvergenceCLM (RingHom.id R) E F
 namespace CompactConvergenceCLM
 
 instance continuousSMul [RingHomSurjective σ] [RingHomIsometric σ]
-    [UniformSpace E] [IsUniformAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F]
+    [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F]
     [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] :
     ContinuousSMul 𝕜₂ (E →SL_c[σ] F) :=
   UniformConvergenceCLM.continuousSMul σ F { S | IsCompact S }
-    (fun _ hs => hs.totallyBounded.isVonNBounded 𝕜₁)
+    (fun _ hs => hs.isVonNBounded 𝕜₁)
 
 instance instContinuousEvalConst [TopologicalSpace E] [TopologicalSpace F]
     [IsTopologicalAddGroup F] : ContinuousEvalConst (E →SL_c[σ] F) E F :=
@@ -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*}
@@ -483,13 +501,11 @@ spaces of continuous (semi)linear maps. -/
 @[simps apply symm_apply toLinearEquiv_apply toLinearEquiv_symm_apply]
 def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
     (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
-{ e₁₂.arrowCongrEquiv e₄₃ with
+{ e₁₂.arrowCongrEquivₛₗ e₄₃ with
     -- given explicitly to help `simps`
     toFun := fun L => (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E))
     -- given explicitly to help `simps`
     invFun := fun L => (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F))
-    map_add' := fun f g => by simp only [add_comp, comp_add]
-    map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ]
     continuous_toFun := ((postcomp F e₄₃.toContinuousLinearMap).comp
       (precomp H e₁₂.symm.toContinuousLinearMap)).continuous
     continuous_invFun := ((precomp H e₁₂.toContinuousLinearMap).comp