feat(topology/algebra/module/strong_operator, analysis/normed_space/o…

…perator_norm): strong operator topology (#16053)

src/analysis/convolution.lean

@@ -940,7 +940,7 @@ lemma convolution_precompR_apply {g : G → E'' →L[𝕜] E'}
   (hf : locally_integrable f μ) (hcg : has_compact_support g) (hg : continuous g)
   (x₀ : G) (x : E'') : (f ⋆[L.precompR E'', μ] g) x₀ x = (f ⋆[L, μ] (λ a, g a x)) x₀  :=
 begin
-  have := hcg.convolution_exists_right (L.precompR E'') hf hg x₀,
+  have := hcg.convolution_exists_right (L.precompR E'' : _) hf hg x₀,
   simp_rw [convolution_def, continuous_linear_map.integral_apply this],
   refl,
 end

src/analysis/normed_space/bounded_linear_maps.lean

@@ -242,7 +242,7 @@ argument of `f`.
 variables {R : Type*}
 variables {𝕜₂ 𝕜' : Type*} [nontrivially_normed_field 𝕜'] [nontrivially_normed_field 𝕜₂]
 variables {M : Type*} [topological_space M]
-variables {σ₁₂ : 𝕜 →+* 𝕜₂} [ring_hom_isometric σ₁₂]
+variables {σ₁₂ : 𝕜 →+* 𝕜₂}
 variables {G' : Type*} [normed_add_comm_group G'] [normed_space 𝕜₂ G'] [normed_space 𝕜' G']
 variables [smul_comm_class 𝕜₂ 𝕜' G']
 
@@ -544,7 +544,7 @@ begin
   refine λ e, is_open.mem_nhds _ (mem_range_self _),
   let O : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : F →L[𝕜] E).comp f,
   have h_O : continuous O := is_bounded_bilinear_map_comp.continuous_right,
-  convert units.is_open.preimage h_O using 1,
+  convert show is_open (O ⁻¹' {x | is_unit x}), from units.is_open.preimage h_O using 1,
   ext f',
   split,
   { rintros ⟨e', rfl⟩,

src/analysis/normed_space/multilinear.lean

@@ -882,8 +882,8 @@ def mk_continuous_linear (f : G →ₗ[𝕜] multilinear_map 𝕜 E G') (C : ℝ
   G →L[𝕜] continuous_multilinear_map 𝕜 E G' :=
 linear_map.mk_continuous
   { to_fun := λ x, (f x).mk_continuous (C * ∥x∥) $ H x,
-    map_add' := λ x y, by { ext1, simp },
-    map_smul' := λ c x, by { ext1, simp } }
+    map_add' := λ x y, by { ext1, simp only [_root_.map_add], refl },
+    map_smul' := λ c x, by { ext1, simp only [smul_hom_class.map_smul], refl } }
   (max C 0) $ λ x, ((f x).mk_continuous_norm_le' _).trans_eq $
     by rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
 

src/analysis/normed_space/operator_norm.lean

@@ -7,6 +7,7 @@ import algebra.algebra.tower
 import analysis.asymptotics.asymptotics
 import analysis.normed_space.linear_isometry
 import analysis.normed_space.riesz_lemma
+import topology.algebra.module.strong_topology
 
 /-!
 # Operator norm on the space of continuous linear maps
@@ -381,14 +382,99 @@ lemma op_norm_smul_le {𝕜' : Type*} [normed_field 𝕜'] [normed_space 𝕜' F
   end))
 
 /-- Continuous linear maps themselves form a seminormed space with respect to
-    the operator norm. -/
-instance to_seminormed_add_comm_group : seminormed_add_comm_group (E →SL[σ₁₂] F) :=
+the operator norm. This is only a temporary definition because we want to replace the topology
+with `continuous_linear_map.topological_space` to avoid diamond issues.
+See Note [forgetful inheritance] -/
+protected def tmp_seminormed_add_comm_group : seminormed_add_comm_group (E →SL[σ₁₂] F) :=
 add_group_seminorm.to_seminormed_add_comm_group
 { to_fun := norm,
   map_zero' := op_norm_zero,
   add_le' := op_norm_add_le,
   neg' := op_norm_neg }
 
+/-- The `pseudo_metric_space` structure on `E →SL[σ₁₂] F` coming from
+`continuous_linear_map.tmp_seminormed_add_comm_group`.
+See Note [forgetful inheritance] -/
+protected def tmp_pseudo_metric_space : pseudo_metric_space (E →SL[σ₁₂] F) :=
+continuous_linear_map.tmp_seminormed_add_comm_group.to_pseudo_metric_space
+
+/-- The `uniform_space` structure on `E →SL[σ₁₂] F` coming from
+`continuous_linear_map.tmp_seminormed_add_comm_group`.
+See Note [forgetful inheritance] -/
+protected def tmp_uniform_space : uniform_space (E →SL[σ₁₂] F) :=
+continuous_linear_map.tmp_pseudo_metric_space.to_uniform_space
+
+/-- The `topological_space` structure on `E →SL[σ₁₂] F` coming from
+`continuous_linear_map.tmp_seminormed_add_comm_group`.
+See Note [forgetful inheritance] -/
+protected def tmp_topological_space : topological_space (E →SL[σ₁₂] F) :=
+continuous_linear_map.tmp_uniform_space.to_topological_space
+
+section tmp
+
+local attribute [-instance] continuous_linear_map.topological_space
+local attribute [-instance] continuous_linear_map.uniform_space
+local attribute [instance] continuous_linear_map.tmp_seminormed_add_comm_group
+
+protected lemma tmp_topological_add_group : topological_add_group (E →SL[σ₁₂] F) :=
+infer_instance
+
+protected lemma tmp_closed_ball_div_subset {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
+  closed_ball (0 : E →SL[σ₁₂] F) (a / b) ⊆
+  {f | ∀ x ∈ closed_ball (0 : E) b, f x ∈ closed_ball (0 : F) a} :=
+begin
+  intros f hf x hx,
+  rw mem_closed_ball_zero_iff at ⊢ hf hx,
+  calc ∥f x∥
+      ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
+  ... ≤ (a/b) * b : mul_le_mul hf hx (norm_nonneg _) (div_pos ha hb).le
+  ... = a : div_mul_cancel a hb.ne.symm
+end
+
+end tmp
+
+protected theorem tmp_topology_eq :
+  (continuous_linear_map.tmp_topological_space : topological_space (E →SL[σ₁₂] F)) =
+  continuous_linear_map.topological_space :=
+begin
+  refine continuous_linear_map.tmp_topological_add_group.ext infer_instance
+    ((@metric.nhds_basis_closed_ball _ continuous_linear_map.tmp_pseudo_metric_space 0).ext
+      (continuous_linear_map.has_basis_nhds_zero_of_basis metric.nhds_basis_closed_ball) _ _),
+  { rcases normed_field.exists_norm_lt_one 𝕜 with ⟨c, hc₀, hc₁⟩,
+    refine λ ε hε, ⟨⟨closed_ball 0 (1 / ∥c∥), ε⟩,
+      ⟨normed_space.is_vonN_bounded_closed_ball _ _ _, hε⟩, λ f hf, _⟩,
+    change ∀ x, _ at hf,
+    simp_rw mem_closed_ball_zero_iff at hf,
+    rw @mem_closed_ball_zero_iff _ seminormed_add_comm_group.to_seminormed_add_group,
+    refine op_norm_le_of_shell' (div_pos one_pos hc₀) hε.le hc₁ (λ x hx₁ hxc, _),
+    rw div_mul_cancel 1 hc₀.ne.symm at hx₁,
+    exact (hf x hxc.le).trans (le_mul_of_one_le_right hε.le hx₁) },
+  { rintros ⟨S, ε⟩ ⟨hS, hε⟩,
+    rw [normed_space.is_vonN_bounded_iff, ← bounded_iff_is_bounded] at hS,
+    rcases hS.subset_ball_lt 0 0 with ⟨δ, hδ, hSδ⟩,
+    exact ⟨ε/δ, div_pos hε hδ, (continuous_linear_map.tmp_closed_ball_div_subset hε hδ).trans $
+      λ f hf x hx, hf x $ hSδ hx⟩ }
+end
+
+protected theorem tmp_uniform_space_eq :
+  (continuous_linear_map.tmp_uniform_space : uniform_space (E →SL[σ₁₂] F)) =
+  continuous_linear_map.uniform_space :=
+begin
+  rw [← @uniform_add_group.to_uniform_space_eq _ continuous_linear_map.tmp_uniform_space,
+      ← @uniform_add_group.to_uniform_space_eq _ continuous_linear_map.uniform_space],
+  congr' 1,
+  exact continuous_linear_map.tmp_topology_eq
+end
+
+instance to_pseudo_metric_space : pseudo_metric_space (E →SL[σ₁₂] F) :=
+continuous_linear_map.tmp_pseudo_metric_space.replace_uniformity
+  (congr_arg _ continuous_linear_map.tmp_uniform_space_eq.symm)
+
+/-- Continuous linear maps themselves form a seminormed space with respect to
+    the operator norm. -/
+instance to_seminormed_add_comm_group : seminormed_add_comm_group (E →SL[σ₁₂] F) :=
+{ dist_eq := continuous_linear_map.tmp_seminormed_add_comm_group.dist_eq }
+
 lemma nnnorm_def (f : E →SL[σ₁₂] F) : ∥f∥₊ = Inf {c | ∀ x, ∥f x∥₊ ≤ c * ∥x∥₊} :=
 begin
   ext,
@@ -1302,12 +1388,7 @@ instance norm_one_class [nontrivial E] : norm_one_class (E →L[𝕜] E) := ⟨n
 /-- Continuous linear maps themselves form a normed space with respect to
     the operator norm. -/
 instance to_normed_add_comm_group [ring_hom_isometric σ₁₂] : normed_add_comm_group (E →SL[σ₁₂] F) :=
-add_group_norm.to_normed_add_comm_group
-{ to_fun := norm,
-  map_zero' := op_norm_zero,
-  neg' := op_norm_neg,
-  add_le' := op_norm_add_le,
-  eq_zero_of_map_eq_zero' := λ f, (op_norm_zero_iff f).1 }
+normed_add_comm_group.of_separation (λ f, (op_norm_zero_iff f).mp)
 
 /-- Continuous linear maps form a normed ring with respect to the operator norm. -/
 instance to_normed_ring : normed_ring (E →L[𝕜] E) :=

src/topology/algebra/module/strong_topology.lean

@@ -0,0 +1,193 @@
+/-
+Copyright (c) 2022 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+import topology.algebra.uniform_convergence
+
+/-!
+# Strong topologies on the space of continuous linear maps
+
+In this file, we define the strong topologies on `E →L[𝕜] F` associated with a family
+`𝔖 : set (set E)` to be the topology of uniform convergence on the elements of `𝔖` (also called
+the topology of `𝔖`-convergence).
+
+The lemma `uniform_convergence_on.has_continuous_smul_of_image_bounded` tells us that this is a
+vector space topology if the continuous linear image of any element of `𝔖` is bounded (in the sense
+of `bornology.is_vonN_bounded`).
+
+We then declare an instance for the case where `𝔖` is exactly the set of all bounded subsets of
+`E`, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of
+bounded convergence"), which coincides with the operator norm topology in the case of
+`normed_space`s.
+
+Other useful examples include the weak-* topology (when `𝔖` is the set of finite sets or the set
+of singletons) and the topology of compact convergence (when `𝔖` is the set of relatively compact
+sets).
+
+## Main definitions
+
+* `continuous_linear_map.strong_topology` is the topology mentioned above for an arbitrary `𝔖`.
+* `continuous_linear_map.topological_space` is the topology of bounded convergence. This is
+  declared as an instance.
+
+## Main statements
+
+* `continuous_linear_map.strong_topology.topological_add_group` and
+  `continuous_linear_map.strong_topology.has_continuous_smul` show that the strong topology
+  makes `E →L[𝕜] F` a topological vector space, with the assumptions on `𝔖` mentioned above.
+* `continuous_linear_map.topological_add_group` and
+  `continuous_linear_map.has_continuous_smul` register these facts as instances for the special
+  case of bounded convergence.
+
+## References
+
+* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987]
+
+## TODO
+
+* show that these topologies are T₂ and locally convex if the topology on `F` is
+
+## Tags
+
+uniform convergence, bounded convergence
+-/
+
+open_locale topological_space
+
+namespace continuous_linear_map
+
+section general
+
+variables {𝕜₁ 𝕜₂ : Type*} [normed_field 𝕜₁] [normed_field 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂)
+  {E : Type*} (F : Type*) [add_comm_group E] [module 𝕜₁ E]
+  [add_comm_group F] [module 𝕜₂ F] [topological_space E]
+
+/-- Given `E` and `F` two topological vector spaces and `𝔖 : set (set E)`, then
+`strong_topology σ F 𝔖` is the "topology of uniform convergence on the elements of `𝔖`" on
+`E →L[𝕜] F`.
+
+If the continuous linear image of any element of `𝔖` is bounded, this makes `E →L[𝕜] F` a
+topological vector space. -/
+def strong_topology [topological_space F] [topological_add_group F]
+  (𝔖 : set (set E)) : topological_space (E →SL[σ] F) :=
+(@uniform_convergence_on.topological_space E F
+  (topological_add_group.to_uniform_space F) 𝔖).induced coe_fn
+
+/-- The uniform structure associated with `continuous_linear_map.strong_topology`. We make sure
+that this has nice definitional properties. -/
+def strong_uniformity [uniform_space F] [uniform_add_group F]
+  (𝔖 : set (set E)) : uniform_space (E →SL[σ] F) :=
+@uniform_space.replace_topology _ (strong_topology σ F 𝔖)
+  ((uniform_convergence_on.uniform_space E F 𝔖).comap coe_fn)
+  (by rw [strong_topology, uniform_add_group.to_uniform_space_eq]; refl)
+
+@[simp] lemma strong_uniformity_topology_eq [uniform_space F] [uniform_add_group F]
+  (𝔖 : set (set E)) :
+  (strong_uniformity σ F 𝔖).to_topological_space = strong_topology σ F 𝔖 :=
+rfl
+
+lemma strong_uniformity.uniform_add_group [uniform_space F] [uniform_add_group F]
+  (𝔖 : set (set E)) : @uniform_add_group (E →SL[σ] F) (strong_uniformity σ F 𝔖) _ :=
+begin
+  letI : uniform_space (E → F) := uniform_convergence_on.uniform_space E F 𝔖,
+  letI : uniform_space (E →SL[σ] F) := strong_uniformity σ F 𝔖,
+  haveI : uniform_add_group (E → F) := uniform_convergence_on.uniform_add_group,
+  rw [strong_uniformity, uniform_space.replace_topology_eq],
+  let φ : (E →SL[σ] F) →+ E → F := ⟨(coe_fn : (E →SL[σ] F) → E → F), rfl, λ _ _, rfl⟩,
+  exact uniform_add_group_comap φ
+end
+
+lemma strong_topology.topological_add_group [topological_space F] [topological_add_group F]
+  (𝔖 : set (set E)) : @topological_add_group (E →SL[σ] F) (strong_topology σ F 𝔖) _ :=
+begin
+  letI : uniform_space F := topological_add_group.to_uniform_space F,
+  haveI : uniform_add_group F := topological_add_comm_group_is_uniform,
+  letI : uniform_space (E →SL[σ] F) := strong_uniformity σ F 𝔖,
+  haveI : uniform_add_group (E →SL[σ] F) := strong_uniformity.uniform_add_group σ F 𝔖,
+  apply_instance
+end
+
+lemma strong_topology.has_continuous_smul [ring_hom_surjective σ] [ring_hom_isometric σ]
+  [topological_space F] [topological_add_group F] [has_continuous_smul 𝕜₂ F] (𝔖 : set (set E))
+  (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (⊆) 𝔖) (h𝔖₃ : ∀ S ∈ 𝔖, bornology.is_vonN_bounded 𝕜₁ S) :
+  @has_continuous_smul 𝕜₂ (E →SL[σ] F) _ _ (strong_topology σ F 𝔖) :=
+begin
+  letI : uniform_space F := topological_add_group.to_uniform_space F,
+  haveI : uniform_add_group F := topological_add_comm_group_is_uniform,
+  letI : topological_space (E → F) := uniform_convergence_on.topological_space E F 𝔖,
+  letI : topological_space (E →SL[σ] F) := strong_topology σ F 𝔖,
+  let φ : (E →SL[σ] F) →ₗ[𝕜₂] E → F := ⟨(coe_fn : (E →SL[σ] F) → E → F), λ _ _, rfl, λ _ _, rfl⟩,
+  exact uniform_convergence_on.has_continuous_smul_induced_of_image_bounded 𝕜₂ E F (E →SL[σ] F)
+    h𝔖₁ h𝔖₂ φ ⟨rfl⟩ (λ u s hs, (h𝔖₃ s hs).image u)
+end
+
+lemma strong_topology.has_basis_nhds_zero_of_basis [topological_space F] [topological_add_group F]
+  {ι : Type*} (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (⊆) 𝔖) {p : ι → Prop}
+  {b : ι → set F} (h : (𝓝 0 : filter F).has_basis p b) :
+  (@nhds (E →SL[σ] F) (strong_topology σ F 𝔖) 0).has_basis
+    (λ Si : set E × ι, Si.1 ∈ 𝔖 ∧ p Si.2)
+    (λ Si, {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}) :=
+begin
+  letI : uniform_space F := topological_add_group.to_uniform_space F,
+  haveI : uniform_add_group F := topological_add_comm_group_is_uniform,
+  rw nhds_induced,
+  exact (uniform_convergence_on.has_basis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap coe_fn
+end
+
+lemma strong_topology.has_basis_nhds_zero [topological_space F] [topological_add_group F]
+  (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on (⊆) 𝔖) :
+  (@nhds (E →SL[σ] F) (strong_topology σ F 𝔖) 0).has_basis
+    (λ SV : set E × set F, SV.1 ∈ 𝔖 ∧ SV.2 ∈ (𝓝 0 : filter F))
+    (λ SV, {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}) :=
+strong_topology.has_basis_nhds_zero_of_basis σ F 𝔖 h𝔖₁ h𝔖₂ (𝓝 0).basis_sets
+
+end general
+
+section bounded_sets
+
+variables {𝕜₁ 𝕜₂ : Type*} [normed_field 𝕜₁] [normed_field 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E F : Type*}
+  [add_comm_group E] [module 𝕜₁ E] [add_comm_group F] [module 𝕜₂ F] [topological_space E]
+
+/-- The topology of bounded convergence on `E →L[𝕜] F`. This coincides with the topology induced by
+the operator norm when `E` and `F` are normed spaces. -/
+instance [topological_space F] [topological_add_group F] : topological_space (E →SL[σ] F) :=
+strong_topology σ F {S | bornology.is_vonN_bounded 𝕜₁ S}
+
+instance [topological_space F] [topological_add_group F] : topological_add_group (E →SL[σ] F) :=
+strong_topology.topological_add_group σ F _
+
+instance [ring_hom_surjective σ] [ring_hom_isometric σ] [topological_space F]
+  [topological_add_group F] [has_continuous_smul 𝕜₂ F] :
+  has_continuous_smul 𝕜₂ (E →SL[σ] F) :=
+strong_topology.has_continuous_smul σ F {S | bornology.is_vonN_bounded 𝕜₁ S}
+  ⟨∅, bornology.is_vonN_bounded_empty 𝕜₁ E⟩
+  (directed_on_of_sup_mem $ λ _ _, bornology.is_vonN_bounded.union)
+  (λ s hs, hs)
+
+instance [uniform_space F] [uniform_add_group F] : uniform_space (E →SL[σ] F) :=
+strong_uniformity σ F {S | bornology.is_vonN_bounded 𝕜₁ S}
+
+instance [uniform_space F] [uniform_add_group F] : uniform_add_group (E →SL[σ] F) :=
+strong_uniformity.uniform_add_group σ F _
+
+protected lemma has_basis_nhds_zero_of_basis [topological_space F]
+  [topological_add_group F] {ι : Type*} {p : ι → Prop} {b : ι → set F}
+  (h : (𝓝 0 : filter F).has_basis p b) :
+  (𝓝 (0 : E →SL[σ] F)).has_basis
+    (λ Si : set E × ι, bornology.is_vonN_bounded 𝕜₁ Si.1 ∧ p Si.2)
+    (λ Si, {f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}) :=
+strong_topology.has_basis_nhds_zero_of_basis σ F
+  {S | bornology.is_vonN_bounded 𝕜₁ S} ⟨∅, bornology.is_vonN_bounded_empty 𝕜₁ E⟩
+  (directed_on_of_sup_mem $ λ _ _, bornology.is_vonN_bounded.union) h
+
+protected lemma has_basis_nhds_zero [topological_space F]
+  [topological_add_group F] :
+  (𝓝 (0 : E →SL[σ] F)).has_basis
+    (λ SV : set E × set F, bornology.is_vonN_bounded 𝕜₁ SV.1 ∧ SV.2 ∈ (𝓝 0 : filter F))
+    (λ SV, {f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}) :=
+continuous_linear_map.has_basis_nhds_zero_of_basis (𝓝 0).basis_sets
+
+end bounded_sets
+
+end continuous_linear_map