feat(Topology/Algebra/StrongTopology): introduce type synonym for abs…

…tract topologies on CLM (#11470)

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -155,36 +155,14 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
       (ContinuousLinearMap.compL 𝕜 Fu G Gu (isoG.symm : G →L[𝕜] Gu)) Bu₀ := rfl
   have Bu_eq : (fun y => Bu (fu y) (gu y)) = isoG.symm ∘ (fun y => B (f y) (g y)) ∘ isoD := by
     ext1 y
-    -- Porting note: the two blocks of `rw`s below were
-    -- ```
-    -- simp only [ContinuousLinearMap.compL_apply, Function.comp_apply,
-    --   ContinuousLinearMap.coe_comp', LinearIsometryEquiv.coe_coe'',
-    --   ContinuousLinearMap.flip_apply, LinearIsometryEquiv.apply_symm_apply]
-    -- ```
-    rw [hBu]
-    iterate 2 rw [ContinuousLinearMap.compL_apply, ContinuousLinearMap.coe_comp',
-      Function.comp_apply]
-    rw [hBu₀]
-    iterate 2 rw [ContinuousLinearMap.flip_apply, ContinuousLinearMap.coe_comp',
-      Function.comp_apply]
-    rw [hfu, Function.comp_apply, LinearIsometryEquiv.coe_coe'', LinearIsometryEquiv.coe_coe'',
-      LinearIsometryEquiv.apply_symm_apply isoE, Function.comp_apply,
-      hgu, LinearIsometryEquiv.coe_coe'', Function.comp_apply,
-      LinearIsometryEquiv.apply_symm_apply isoF]
-    simp only [Function.comp_apply]
+    simp [hBu, hBu₀, hfu, hgu]
   -- All norms are preserved by the lifting process.
   have Bu_le : ‖Bu‖ ≤ ‖B‖ := by
     refine' ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun y => _
     refine' ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun x => _
-    set_option tactic.skipAssignedInstances false in
-    simp only [Bu, ContinuousLinearMap.compL_apply, ContinuousLinearMap.coe_comp',
-      Function.comp_apply, LinearIsometryEquiv.coe_coe'', ContinuousLinearMap.flip_apply,
+    simp only [hBu, hBu₀, compL_apply, coe_comp', Function.comp_apply,
+      ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe, flip_apply,
       LinearIsometryEquiv.norm_map]
-    rw [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.compL_apply,
-      ContinuousLinearMap.coe_comp', Function.comp_apply]
-    iterate 2 rw [ContinuousLinearMap.flip_apply, ContinuousLinearMap.coe_comp',
-      Function.comp_apply]
-    simp only [LinearIsometryEquiv.coe_coe'', LinearIsometryEquiv.norm_map]
     calc
       ‖B (isoE y) (isoF x)‖ ≤ ‖B (isoE y)‖ * ‖isoF x‖ := ContinuousLinearMap.le_opNorm _ _
       _ ≤ ‖B‖ * ‖isoE y‖ * ‖isoF x‖ := by gcongr; apply ContinuousLinearMap.le_opNorm

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -366,10 +366,10 @@ variable (p : FormalMultilinearSeries 𝕜 E F)
 open Fintype ContinuousLinearMap in
 theorem derivSeries_apply_diag (n : ℕ) (x : E) :
     derivSeries p n (fun _ ↦ x) x = (n + 1) • p (n + 1) fun _ ↦ x := by
-  simp only [derivSeries, strongUniformity_topology_eq, compFormalMultilinearSeries_apply,
-    changeOriginSeries, compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
-    LinearIsometryEquiv.coe_coe, Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum,
-    coe_sum', Finset.sum_apply, continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
+  simp only [derivSeries, compFormalMultilinearSeries_apply, changeOriginSeries,
+    compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
+    Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum, coe_sum', Finset.sum_apply,
+    continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
   convert Finset.sum_const _
   · rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
   · rw [← card, card_subtype, ← Finset.powerset_univ, ← Finset.powersetCard_eq_filter,

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -637,9 +637,8 @@ lemma _root_.Function.HasTemperateGrowth.of_fderiv {f : E → F}
   rcases n with rfl|m
   · exact ⟨k, C, fun x ↦ by simpa using h x⟩
   · rcases h'f.2 m with ⟨k', C', h'⟩
-    refine ⟨k', C', fun x ↦ ?_⟩
-    simpa only [ContinuousLinearMap.strongUniformity_topology_eq, Function.comp_apply,
-      LinearIsometryEquiv.norm_map, iteratedFDeriv_succ_eq_comp_right] using h' x
+    refine ⟨k', C', ?_⟩
+    simpa [iteratedFDeriv_succ_eq_comp_right] using h'
 
 lemma _root_.Function.HasTemperateGrowth.zero :
     Function.HasTemperateGrowth (fun _ : E ↦ (0 : F)) := by

Mathlib/Analysis/LocallyConvex/StrongTopology.lean

@@ -32,42 +32,44 @@ open Topology UniformConvergence
 
 variable {R 𝕜₁ 𝕜₂ E F : Type*}
 
-namespace ContinuousLinearMap
-
 variable [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F]
   [TopologicalAddGroup F]
 
 section General
 
+namespace UniformConvergenceCLM
+
 variable (R)
 variable [OrderedSemiring R]
 variable [NormedField 𝕜₁] [NormedField 𝕜₂] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂}
 variable [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F]
 
-theorem strongTopology.locallyConvexSpace (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty)
+theorem locallyConvexSpace (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty)
     (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
-    @LocallyConvexSpace R (E →SL[σ] F) _ _ _ (strongTopology σ F 𝔖) := by
-  letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
-  haveI : TopologicalAddGroup (E →SL[σ] F) := strongTopology.topologicalAddGroup _ _ _
+    LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖) := by
   apply LocallyConvexSpace.ofBasisZero _ _ _ _
-    (strongTopology.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
+    (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
       (LocallyConvexSpace.convex_basis_zero R F)) _
   rintro ⟨S, V⟩ ⟨_, _, hVconvex⟩ f hf g hg a b ha hb hab x hx
   exact hVconvex (hf x hx) (hg x hx) ha hb hab
-#align continuous_linear_map.strong_topology.locally_convex_space ContinuousLinearMap.strongTopology.locallyConvexSpace
+#align continuous_linear_map.strong_topology.locally_convex_space UniformConvergenceCLM.locallyConvexSpace
+
+end UniformConvergenceCLM
 
 end General
 
 section BoundedSets
 
+namespace ContinuousLinearMap
+
 variable [OrderedSemiring R]
 variable [NormedField 𝕜₁] [NormedField 𝕜₂] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂}
 variable [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F]
 
-instance : LocallyConvexSpace R (E →SL[σ] F) :=
-  strongTopology.locallyConvexSpace R _ ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
+instance instLocallyConvexSpace : LocallyConvexSpace R (E →SL[σ] F) :=
+  UniformConvergenceCLM.locallyConvexSpace R _ ⟨∅, Bornology.isVonNBounded_empty 𝕜₁ E⟩
     (directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union)
 
-end BoundedSets
-
 end ContinuousLinearMap
+
+end BoundedSets