feat(Analysis/Normed/Module): add bornology and T2 instances for WeakSpace

Mathlib.lean

@@ -1963,7 +1963,7 @@ public import Mathlib.Analysis.LocallyConvex.Polar
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
 public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.Analysis.LocallyConvex.StrongTopology
-public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 public import Mathlib.Analysis.LocallyConvex.WeakSpace
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
@@ -2097,6 +2097,7 @@ public import Mathlib.Analysis.Normed.Module.Shrink
 public import Mathlib.Analysis.Normed.Module.Span
 public import Mathlib.Analysis.Normed.Module.TransferInstance
 public import Mathlib.Analysis.Normed.Module.WeakDual
+public import Mathlib.Analysis.Normed.Module.WeakSpace
 public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Operator.Asymptotics
 public import Mathlib.Analysis.Normed.Operator.Banach
@@ -7240,6 +7241,7 @@ public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 public import Mathlib.Topology.Algebra.Monoid
 public import Mathlib.Topology.Algebra.Monoid.AddChar
 public import Mathlib.Topology.Algebra.Monoid.Defs

Mathlib/Analysis/LocallyConvex/WeakDual.lean → Mathlib/Analysis/LocallyConvex/WeakBilin.lean

@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 
 /-!
-# Weak Dual in Topological Vector Spaces
+# Weak Bilinear Topologies in Topological Vector Spaces
 
 We prove that the weak topology induced by a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is locally
 convex and we explicitly give a neighborhood basis in terms of the family of seminorms
@@ -28,7 +28,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 * `LinearMap.hasBasis_weakBilin`: the seminorm balls of `B.toSeminormFamily` form a
   neighborhood basis of `0` in the weak topology.
-* `LinearMap.toSeminormFamily.withSeminorms`: the topology of a weak space is induced by the
+* `LinearMap.weakBilin_withSeminorms`: the topology of a weak space is induced by the
   family of seminorms `B.toSeminormFamily`.
 * `WeakBilin.locallyConvexSpace`: a space endowed with a weak topology is locally convex.
 * `LinearMap.rightDualEquiv`: When `B` is right-separating, `F` is linearly equivalent to the
@@ -43,7 +43,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 ## Tags
 
-weak dual, seminorm
+weak bilinear, seminorm
 -/
 
 @[expose] public section

Mathlib/Analysis/LocallyConvex/WeakSpace.lean

@@ -1,25 +1,65 @@
 /-
 Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jireh Loreaux
+Authors: Jireh Loreaux, Michał Świętek
 -/
 module
 
 public import Mathlib.Analysis.LocallyConvex.Separation
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.LinearAlgebra.Dual.Defs
-public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
-/-! # Closures of convex sets in locally convex spaces
+/-! # Weak topology on normed spaces: seminorm family and convex closures
 
-This file contains the standard result that if `E` is a vector space with two locally convex
+## Seminorm family
+
+The weak topology on `WeakSpace 𝕜 E` is generated by the seminorm family `fun f x ↦ ‖f x‖`
+indexed by `StrongDual 𝕜 E`. This follows from the general `LinearMap.weakBilin_withSeminorms`
+applied to the flipped `topDualPairing`.
+
+## Closures of convex sets
+
+This file also contains the standard result that if `E` is a vector space with two locally convex
 topologies, then the closure of a convex set is the same in either topology, provided they have the
 same collection of continuous linear functionals. In particular, the weak closure of a convex set
 in a locally convex space coincides with the closure in the original topology.
 Of course, we phrase this in terms of linear maps between locally convex spaces, rather than
 creating two separate topologies on the same space.
 -/
 
-public section
+@[expose] public section
+
+section Seminorms
+
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+  [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
+
+namespace WeakSpace
+
+set_option backward.isDefEq.respectTransparency false in
+variable (𝕜 E) in
+/-- The family of seminorms on `WeakSpace 𝕜 E` given by `fun f x ↦ ‖f x‖`, indexed by
+`StrongDual 𝕜 E`. This is the seminorm family associated to the weak topology via the
+flipped `topDualPairing`. -/
+def seminormFamily : SeminormFamily 𝕜 (WeakSpace 𝕜 E) (StrongDual 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.toSeminormFamily
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+@[simp]
+lemma seminormFamily_apply (f : StrongDual 𝕜 E) (x : WeakSpace 𝕜 E) :
+    seminormFamily 𝕜 E f x = ‖f x‖ := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+variable (𝕜 E) in
+lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.weakBilin_withSeminorms
+
+end WeakSpace
+
+end Seminorms
 
 variable {𝕜 E F : Type*}
 variable [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]

Mathlib/Analysis/Normed/Module/WeakSpace.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Michał Świętek. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Świętek
+-/
+module
+
+public import Mathlib.Analysis.Normed.Module.HahnBanach
+public import Mathlib.Analysis.Normed.Module.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakSpace
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
+
+/-!
+# Normed space instances for `WeakSpace`
+
+This file provides basic instances for `WeakSpace 𝕜 E` in the setting of normed spaces.
+
+The file equips `WeakSpace 𝕜 E` with the norm bornology inherited from `E`, so that `IsBounded`
+refers to norm boundedness. This is a pragmatic choice discussed further in the implementation
+notes.
+
+## Main definitions
+
+* `WeakSpace.instBornology`: The norm bornology on `WeakSpace 𝕜 E`, inherited from `E`.
+* `WeakSpace.seminormFamily`: The family of seminorms `fun f x ↦ ‖f x‖` generating the weak
+  topology, indexed by `StrongDual 𝕜 E`.
+* `WeakSpace.instT2Space`: The weak topology on a normed space over `RCLike` is Hausdorff,
+  via Hahn–Banach separation.
+
+## Main results
+
+### Topology comparison
+* `WeakSpace.norm_topology_le_weakSpace_topology`: The weak topology is coarser than the norm
+  topology.
+
+### Bornology and pointwise bounds
+* `WeakSpace.isBounded_iff_isVonNBounded`: Equivalence of norm and weak boundedness for
+  normed spaces over `RCLike`.
+
+## Implementation notes
+
+* **Bornology choice:** The `Bornology` instance on `WeakSpace 𝕜 E` is inherited from `E` via
+  `inferInstanceAs` and corresponds to the norm bornology. While the natural bornology for a
+  weak topology is technically the von Neumann bornology (pointwise boundedness), we use the
+  norm bornology for several pragmatic reasons:
+  1. **Practicality:** In the normed setting, "bounded" is almost universally synonymous with
+     "norm-bounded". This allows `IsBounded` to be used directly.
+  2. **Clarity:** It preserves a clear distinction between norm-boundedness (`IsBounded`) and
+     topological weak boundedness (`IsVonNBounded`).
+  3. **Consistency:** By the Uniform Boundedness Principle, these notions coincide whenever
+     `𝕜` is `RCLike` (`isBounded_iff_isVonNBounded`). No `[CompleteSpace E]` assumption is
+     needed because `banach_steinhaus` is applied to the inclusion in the double dual, whose
+     domain `StrongDual 𝕜 E` is always complete when `𝕜` is `RCLike`.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Bornology Topology
+
+namespace WeakSpace
+
+section NontriviallyNormedField
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- The norm bornology on `WeakSpace 𝕜 E`, inherited from `E`. -/
+instance instBornology : Bornology (WeakSpace 𝕜 E) := inferInstanceAs (Bornology E)
+
+/-- A set in `WeakSpace 𝕜 E` is bounded iff its image in `E` is bounded. -/
+@[simp]
+theorem isBounded_toE_preimage {s : Set E} :
+    IsBounded (⇑(toWeakSpace 𝕜 E).symm ⁻¹' s) ↔ IsBounded s :=
+  Iff.rfl
+
+/-- A set in `E` is bounded iff its image in `WeakSpace 𝕜 E` is bounded. -/
+@[simp]
+theorem isBounded_toWeakSpace_preimage {s : Set (WeakSpace 𝕜 E)} :
+    IsBounded (⇑(toWeakSpace 𝕜 E) ⁻¹' s) ↔ IsBounded s :=
+  Iff.rfl
+
+/-- The weak topology on a normed space is coarser than the norm topology. -/
+theorem norm_topology_le_weakSpace_topology :
+    (UniformSpace.toTopologicalSpace : TopologicalSpace E) ≤
+      (inferInstance : TopologicalSpace (WeakSpace 𝕜 E)) := by
+  convert (toWeakSpaceCLM 𝕜 E).continuous.le_induced
+  exact induced_id.symm
+
+end NontriviallyNormedField
+
+section RCLike
+
+variable (𝕜 : Type*) [RCLike 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- The weak topology on a normed space over `RCLike` is T2 (Hausdorff). This follows from
+Hahn–Banach: the continuous linear functionals separate points. -/
+instance instT2Space : T2Space (WeakSpace 𝕜 E) :=
+  (WeakBilin.isEmbedding (B := (topDualPairing 𝕜 E).flip) fun x y h => by
+    obtain ⟨g, _, hg⟩ := exists_dual_vector'' 𝕜 (x - y)
+    rw [map_sub, show g x = g y from LinearMap.ext_iff.mp h g, sub_self] at hg
+    exact sub_eq_zero.mp (norm_eq_zero.mp (by exact_mod_cast hg.symm))).t2Space
+
+set_option backward.isDefEq.respectTransparency false in
+/-- By the Uniform Boundedness Principle, norm-boundedness (the default bornology)
+and pointwise-boundedness (`IsVonNBounded`) coincide on the weak space of a normed space
+over `RCLike`. -/
+theorem isBounded_iff_isVonNBounded {s : Set (WeakSpace 𝕜 E)} :
+    IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s := by
+  constructor
+  · exact fun h => ((NormedSpace.isVonNBounded_iff (E := E) (𝕜 := 𝕜)).mpr h).of_topologicalSpace_le
+      norm_topology_le_weakSpace_topology
+  · intro h_vN
+    have h_ptwise := (WeakSpace.withSeminorms 𝕜 E).isVonNBounded_iff_seminorm_bounded.mp h_vN
+    obtain ⟨C, hC⟩ := banach_steinhaus
+      (g := fun i : s ↦ NormedSpace.inclusionInDoubleDual 𝕜 E i.val) fun f ↦
+      let ⟨M, _, hM⟩ := h_ptwise f
+      ⟨M, fun i ↦ le_of_lt (hM i.val i.property)⟩
+    suffices @IsBounded E _ s from this
+    rw [isBounded_iff_forall_norm_le]
+    exact ⟨C, fun x hx ↦ by
+      rw [← (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map x]
+      exact hC ⟨x, hx⟩⟩
+
+end RCLike
+
+end WeakSpace

Mathlib/Topology/Algebra/Module/WeakDual.lean

@@ -8,32 +8,20 @@ module
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMap
 public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
 /-!
 # Weak dual topology
 
-We continue in the setting of `Mathlib/Topology/Algebra/Module/WeakBilin.lean`,
-which defines the weak topology given two vector spaces `E` and `F` over a commutative semiring
-`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarsest topology
-such that for all `y : F` every map `fun x => B x y` is continuous.
-
-In this file, we consider two special cases.
-In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology,
-`WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the
-weak topology `WeakSpace 𝕜 E := E`.
+This file defines the weak-* (weak dual) topology on the continuous dual `E →L[𝕜] 𝕜`.
+It is the coarsest topology such that for all `z : E` every evaluation map
+`fun v => v z` is continuous.
 
 ## Main definitions
 
-The main definitions are the types `WeakDual 𝕜 E` and `WeakSpace 𝕜 E`,
-with the respective topology instances on it.
-
-* `WeakDual 𝕜 E` is a type synonym for `Dual 𝕜 E` (when the latter is defined): both are equal to
-  the type `E →L[𝕜] 𝕜` of continuous linear maps from a module `E` over `𝕜` to the ring `𝕜`.
+* `WeakDual 𝕜 E` is a type synonym for `E →L[𝕜] 𝕜` (equal to `Dual 𝕜 E`).
 * The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual 𝕜 E`, i.e., the
   coarsest topology making the evaluation maps at all `z : E` continuous.
-* `WeakSpace 𝕜 E` is a type synonym for `E` (when the latter is defined).
-* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
-  coarsest topology such that all `v : dual 𝕜 E` remain continuous.
 
 ## References
 
@@ -132,103 +120,16 @@ end Ring
 
 end WeakDual
 
-/-- The weak topology is the topology coarsest topology on `E` such that all functionals
-`fun x => v x` are continuous. -/
-def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
-  WeakBilin (topDualPairing 𝕜 E).flip
-deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
-
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
-namespace WeakSpace
-
-instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
-  WeakBilin.instModule' (topDualPairing 𝕜 E).flip
-
-instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
-    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
-
-instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instContinuousSMul _
-
-variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
-
-/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
-their weak topologies. -/
-def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
-  { f with
-    cont :=
-      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
-
-theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
-  rfl
-
-@[simp]
-theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
-  rfl
-
-end WeakSpace
-
-variable (𝕜 E) in
-/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. -/
-def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
-
-variable (𝕜 E) in
-/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
-This definition implements it as a continuous linear map. -/
-def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
-  __ := toWeakSpace 𝕜 E
-  cont := by
-    apply WeakBilin.continuous_of_continuous_eval
-    exact ContinuousLinearMap.continuous
-
-variable (𝕜 E) in
-@[simp]
-theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
-    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
-
-theorem toWeakSpaceCLM_bijective :
-    Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
-  (toWeakSpace 𝕜 E).bijective
-
-/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
-theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
-  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
-    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
-
-/-- A set in `E` which is open in the weak topology is open. -/
-theorem WeakSpace.isOpen_of_isOpen (V : Set E)
-    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
-  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
-
 theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α → WeakDual 𝕜 E}
     {x : WeakDual 𝕜 E} :
     Tendsto f l (𝓝 x) ↔
       ∀ y, Tendsto (fun i => topDualPairing 𝕜 E (f i) y) l (𝓝 (topDualPairing 𝕜 E x y)) :=
   WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective
 
 end Semiring
-
-section Ring
-
-namespace WeakSpace
-
-variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
-
-instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
-
-end WeakSpace
-
-end Ring