From 3f10379df52f7593b4187b32c08f888d0af137b1 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:22:41 +0100
Subject: [PATCH 01/10] Rename WeakDual to WeakBilin

---
 Mathlib.lean                                                   | 3 ++-
 .../Analysis/LocallyConvex/{WeakDual.lean => WeakBilin.lean}   | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)
 rename Mathlib/Analysis/LocallyConvex/{WeakDual.lean => WeakBilin.lean} (99%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 09a2198e928739..47f0e25aeafcd3 100644
--- a/Mathlib.lean
+++ b/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
@@ -7240,6 +7240,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
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
similarity index 99%
rename from Mathlib/Analysis/LocallyConvex/WeakDual.lean
rename to Mathlib/Analysis/LocallyConvex/WeakBilin.lean
index f42be09aeb6c1f..4115f172d9f150 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/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

From 35104dbf50a2ef3a36748c032d7a94cde1ac54b2 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:24:12 +0100
Subject: [PATCH 02/10] Add seminorms

---
 Mathlib/Analysis/LocallyConvex/WeakSpace.lean | 50 +++++++++++++++++--
 1 file changed, 45 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
index a20819b1f86a82..9d2afe956a9fe6 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
@@ -1,17 +1,26 @@
 /-
 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.
@@ -19,7 +28,38 @@ Of course, we phrase this in terms of linear maps between locally convex spaces,
 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]

From 17aa2d93a7b33b6b061e4fd64be4a778215e98f9 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:24:24 +0100
Subject: [PATCH 03/10] Split weakdual

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 109 +-------------
 .../Topology/Algebra/Module/WeakSpace.lean    | 137 ++++++++++++++++++
 2 files changed, 142 insertions(+), 104 deletions(-)
 create mode 100644 Mathlib/Topology/Algebra/Module/WeakSpace.lean

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 9188ee7caf0b2d..f31c0f8c6a7153 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/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,82 +120,12 @@ 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) ↔
@@ -215,20 +133,3 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
   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
diff --git a/Mathlib/Topology/Algebra/Module/WeakSpace.lean b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
new file mode 100644
index 00000000000000..164511adb9363f
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2021 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä, Moritz Doll
+-/
+module
+
+public import Mathlib.LinearAlgebra.BilinearMap
+public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Topology.Algebra.Module.WeakBilin
+
+/-!
+# Weak topology
+
+This file defines the weak topology on a topological vector space `E`.
+It is the coarsest topology on `E` such that all continuous linear functionals
+`fun x => v x` for `v : E →L[𝕜] 𝕜` remain continuous.
+
+## Main definitions
+
+* `WeakSpace 𝕜 E` is a type synonym for `E`.
+* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
+  coarsest topology such that all `v : E →L[𝕜] 𝕜` remain continuous.
+* `toWeakSpace`: The canonical linear equivalence `E ≃ₗ[𝕜] WeakSpace 𝕜 E`.
+* `toWeakSpaceCLM`: The identity mapping as a continuous linear map `E →L[𝕜] WeakSpace 𝕜 E`.
+
+## References
+
+* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
+
+## Tags
+
+weak topology, duality
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Filter Topology
+
+variable {α 𝕜 𝕝 E F : Type*}
+
+/-- 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
+
+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

From 70aa8c42f3f969eee2cf0bbe6d69818bd99cc94f Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:45:28 +0100
Subject: [PATCH 04/10] Fix comments.

---
 Mathlib/Analysis/LocallyConvex/WeakBilin.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/LocallyConvex/WeakBilin.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
index 4115f172d9f150..e5dfa590ad0f20 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
@@ -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

From 3d0542f542cdee83915eed74990fd76e3831b62e Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Sat, 7 Mar 2026 20:50:24 +0000
Subject: [PATCH 05/10] Register bornology.

---
 Mathlib/Analysis/Normed/Module/WeakSpace.lean | 59 +++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 Mathlib/Analysis/Normed/Module/WeakSpace.lean

diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
new file mode 100644
index 00000000000000..73b732d0db34d5
--- /dev/null
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -0,0 +1,59 @@
+/-
+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
+
+/-!
+# Normed space instances for `WeakSpace`
+
+This file provides basic instances for `WeakSpace 𝕜 E` in the setting of normed spaces.
+
+## Main definitions
+
+* `WeakSpace.instBornology`: The norm bornology on `WeakSpace 𝕜 E`, inherited from `E`.
+* `WeakSpace.instT2Space`: The weak topology on a normed space over `RCLike` is Hausdorff,
+  via Hahn–Banach separation.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Bornology Topology
+
+namespace WeakSpace
+
+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
+
+variable (𝕜) [RCLike 𝕜] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+/-- 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 𝕜 F) :=
+  (WeakBilin.isEmbedding (B := (topDualPairing 𝕜 F).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
+
+end WeakSpace

From f40979a90b96c1fd1216eff9c84e7c9be0b0075f Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Sat, 7 Mar 2026 21:43:42 +0000
Subject: [PATCH 06/10] isVonNBounded_iff_forall_eval_bounded

---
 Mathlib/Analysis/Normed/Module/WeakSpace.lean | 72 ++++++++++++++++++-
 1 file changed, 71 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
index 73b732d0db34d5..d13738d2e8bfa1 100644
--- a/Mathlib/Analysis/Normed/Module/WeakSpace.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -28,6 +28,8 @@ open Bornology Topology
 
 namespace WeakSpace
 
+section NontriviallyNormedField
+
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
@@ -46,7 +48,12 @@ theorem isBounded_toWeakSpace_preimage {s : Set (WeakSpace 𝕜 E)} :
     IsBounded (⇑(toWeakSpace 𝕜 E) ⁻¹' s) ↔ IsBounded s :=
   Iff.rfl
 
-variable (𝕜) [RCLike 𝕜] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+end NontriviallyNormedField
+
+section RCLike
+
+variable (𝕜 : Type*) [RCLike 𝕜]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 /-- The weak topology on a normed space over `RCLike` is T2 (Hausdorff). This follows from
 Hahn–Banach: the continuous linear functionals separate points. -/
@@ -56,4 +63,67 @@ instance instT2Space : T2Space (WeakSpace 𝕜 F) :=
     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
 
+/-- A set in `WeakSpace 𝕜 F` is von Neumann bounded iff it is bounded under
+every continuous linear functional. -/
+theorem isVonNBounded_iff_forall_eval_bounded {s : Set (WeakSpace 𝕜 F)} :
+    Bornology.IsVonNBounded 𝕜 s ↔ ∀ f : StrongDual 𝕜 F, ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
+  constructor
+  · -- Forward: vonN bounded → each eval is bounded
+    intro hs f
+    -- f is continuous on WeakSpace
+    have hcont : Continuous fun x : WeakSpace 𝕜 F => f x :=
+      WeakBilin.eval_continuous _ f
+    -- f⁻¹'(ball 0 1) is a weak neighborhood of 0
+    have hmem : (fun x : WeakSpace 𝕜 F => f x) ⁻¹' Metric.ball 0 1 ∈
+        𝓝 (0 : WeakSpace 𝕜 F) :=
+      hcont.continuousAt.preimage_mem_nhds (by
+        change Metric.ball 0 1 ∈ 𝓝 ((f : F →L[𝕜] 𝕜) 0)
+        rw [map_zero]; exact Metric.ball_mem_nhds 0 one_pos)
+    -- This neighborhood absorbs s
+    obtain ⟨r, hr, hab⟩ := (hs hmem).exists_pos
+    refine ⟨r, fun x hx => ?_⟩
+    -- Use (r : 𝕜) which has norm r
+    have hr_norm : ‖(↑r : 𝕜)‖ = r := by rw [RCLike.norm_ofReal, abs_of_pos hr]
+    have hr_ne : (↑r : 𝕜) ≠ 0 := by exact_mod_cast hr.ne'
+    have hxV := hab (↑r : 𝕜) (by rw [hr_norm]) hx
+    rw [Set.mem_smul_set_iff_inv_smul_mem₀ hr_ne] at hxV
+    simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right] at hxV
+    have hfsmul : f ((↑r : 𝕜)⁻¹ • x) = (↑r : 𝕜)⁻¹ • f x := map_smul f (↑r : 𝕜)⁻¹ (x : F)
+    rw [hfsmul, norm_smul, norm_inv, hr_norm] at hxV
+    linarith [inv_mul_lt_iff₀ hr |>.mp hxV]
+  · -- Backward: each eval bounded → vonN bounded
+    intro h V hV
+    -- V ∈ nhds 0 in the weak topology (= induced topology from pi)
+    let φ : WeakSpace 𝕜 F → (StrongDual 𝕜 F → 𝕜) := fun x f => f x
+    have hφ0 : φ 0 = 0 := funext fun f => map_zero f
+    -- nhds 0 in WeakSpace = comap φ (nhds 0) in pi
+    rw [show 𝓝 (0 : WeakSpace 𝕜 F) = Filter.comap φ (𝓝 0) from
+      hφ0 ▸ nhds_induced φ 0, Filter.mem_comap] at hV
+    obtain ⟨U, hU, hUV⟩ := hV
+    rw [nhds_pi, Filter.mem_pi] at hU
+    obtain ⟨I, hI, t, ht, htU⟩ := hU
+    -- Suffices to show the smaller preimage absorbs s
+    apply Absorbs.mono_left _ (Set.Subset.trans (Set.preimage_mono htU) hUV)
+    -- Convert preimage of Set.pi to biInter of preimages
+    have hpi : φ ⁻¹' I.pi t = ⋂ f ∈ I, (fun (x : WeakSpace 𝕜 F) => f x) ⁻¹' t f := by
+      ext x; simp [Set.mem_pi, φ]
+    rw [hpi, hI.absorbs_biInter]
+    intro f hf
+    -- Show each preimage absorbs s via the image being vonN bounded
+    obtain ⟨r, hr⟩ := h f
+    have h_vonN : Bornology.IsVonNBounded 𝕜 ((fun x : WeakSpace 𝕜 F => f x) '' s) :=
+      NormedSpace.image_isVonNBounded_iff (𝕜 := 𝕜).mpr ⟨r, hr⟩
+    have h_abs := h_vonN (ht f)
+    -- Convert: Absorbs 𝕜 (t f) (f '' s) → Absorbs 𝕜 (f⁻¹' t f) s
+    rw [absorbs_iff_eventually_cobounded_mapsTo] at h_abs ⊢
+    exact h_abs.mono fun c hc x hx => by
+      simp only [Set.mem_preimage]
+      have : f (c⁻¹ • x) = c⁻¹ • f x := map_smul f c⁻¹ (x : F)
+      rw [this]
+      exact hc (Set.mem_image_of_mem _ hx)
+
+
+
+end RCLike
+
 end WeakSpace

From bd415f0763b49bd64ae5ba3e91bfcf74de1b4f9e Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Sat, 7 Mar 2026 21:47:29 +0000
Subject: [PATCH 07/10] isBounded_iff_isVonNBounded

---
 Mathlib/Analysis/Normed/Module/WeakSpace.lean | 33 ++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
index d13738d2e8bfa1..153a2b5bf901eb 100644
--- a/Mathlib/Analysis/Normed/Module/WeakSpace.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Normed.Module.HahnBanach
 public import Mathlib.Analysis.Normed.Module.WeakDual
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 
 /-!
 # Normed space instances for `WeakSpace`
@@ -122,7 +123,37 @@ theorem isVonNBounded_iff_forall_eval_bounded {s : Set (WeakSpace 𝕜 F)} :
       rw [this]
       exact hc (Set.mem_image_of_mem _ hx)
 
-
+/-- The norm bornology and the weak von Neumann bornology coincide.
+This is a consequence of the Uniform Boundedness Principle applied to the
+image of F in its double dual. -/
+theorem isBounded_iff_isVonNBounded {s : Set (WeakSpace 𝕜 F)} :
+    IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s := by
+  constructor
+  · -- Forward: norm bounded → vonN bounded in weak topology
+    intro h
+    rw [isVonNBounded_iff_forall_eval_bounded]
+    intro f
+    -- Extract a norm bound from IsBounded (the bornology on WeakSpace is the norm bornology)
+    obtain ⟨C, hC⟩ := (isBounded_iff_forall_norm_le (E := F)).mp h
+    exact ⟨‖f‖ * C, fun x hx => (f.le_opNorm x).trans (by gcongr; exact hC x hx)⟩
+  · -- Backward: vonN bounded in weak → norm bounded (via Banach-Steinhaus)
+    intro h_vN
+    rw [isVonNBounded_iff_forall_eval_bounded] at h_vN
+    -- View elements of s as functionals on the dual via inclusionInDoubleDual
+    -- Pointwise boundedness: for each f : StrongDual 𝕜 F, ‖(inclusionInDoubleDual x) f‖ ≤ r
+    have h_ptwise : ∀ f : StrongDual 𝕜 F, ∃ C, ∀ x : (toWeakSpace 𝕜 F ⁻¹' s),
+        ‖NormedSpace.inclusionInDoubleDual 𝕜 F x f‖ ≤ C := by
+      intro f
+      obtain ⟨r, hr⟩ := h_vN f
+      exact ⟨r, fun ⟨x, hx⟩ => by simp only [NormedSpace.dual_def]; exact hr x hx⟩
+    -- Banach-Steinhaus: uniform bound on operator norms
+    obtain ⟨C, hC⟩ := banach_steinhaus h_ptwise
+    -- Since inclusionInDoubleDualLi is an isometry, ‖x‖ = ‖inclusionInDoubleDual x‖ ≤ C
+    suffices @IsBounded F _ 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
 

From 01454cf318004d38a9071ef34191cb9eed7c0a7f Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Sat, 7 Mar 2026 22:06:12 +0000
Subject: [PATCH 08/10] Polish comments.

---
 Mathlib/Analysis/Normed/Module/WeakSpace.lean | 71 +++++++------------
 1 file changed, 25 insertions(+), 46 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
index 153a2b5bf901eb..98be07c3a49925 100644
--- a/Mathlib/Analysis/Normed/Module/WeakSpace.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -54,102 +54,81 @@ end NontriviallyNormedField
 section RCLike
 
 variable (𝕜 : Type*) [RCLike 𝕜]
-variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+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 𝕜 F) :=
-  (WeakBilin.isEmbedding (B := (topDualPairing 𝕜 F).flip) fun x y h => by
+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
 
-/-- A set in `WeakSpace 𝕜 F` is von Neumann bounded iff it is bounded under
+/-- A set in `WeakSpace 𝕜 E` is von Neumann bounded iff it is bounded under
 every continuous linear functional. -/
-theorem isVonNBounded_iff_forall_eval_bounded {s : Set (WeakSpace 𝕜 F)} :
-    Bornology.IsVonNBounded 𝕜 s ↔ ∀ f : StrongDual 𝕜 F, ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
+theorem isVonNBounded_iff_forall_eval_bounded {s : Set (WeakSpace 𝕜 E)} :
+    Bornology.IsVonNBounded 𝕜 s ↔ ∀ f : StrongDual 𝕜 E, ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
   constructor
-  · -- Forward: vonN bounded → each eval is bounded
-    intro hs f
-    -- f is continuous on WeakSpace
-    have hcont : Continuous fun x : WeakSpace 𝕜 F => f x :=
-      WeakBilin.eval_continuous _ f
-    -- f⁻¹'(ball 0 1) is a weak neighborhood of 0
-    have hmem : (fun x : WeakSpace 𝕜 F => f x) ⁻¹' Metric.ball 0 1 ∈
-        𝓝 (0 : WeakSpace 𝕜 F) :=
+  · intro hs f
+    have hcont : Continuous fun x : WeakSpace 𝕜 E => f x := WeakBilin.eval_continuous _ f
+    have hmem : (fun x : WeakSpace 𝕜 E => f x) ⁻¹' Metric.ball 0 1 ∈ 𝓝 (0 : WeakSpace 𝕜 E) :=
       hcont.continuousAt.preimage_mem_nhds (by
-        change Metric.ball 0 1 ∈ 𝓝 ((f : F →L[𝕜] 𝕜) 0)
+        change Metric.ball 0 1 ∈ 𝓝 ((f : E →L[𝕜] 𝕜) 0)
         rw [map_zero]; exact Metric.ball_mem_nhds 0 one_pos)
-    -- This neighborhood absorbs s
     obtain ⟨r, hr, hab⟩ := (hs hmem).exists_pos
     refine ⟨r, fun x hx => ?_⟩
-    -- Use (r : 𝕜) which has norm r
     have hr_norm : ‖(↑r : 𝕜)‖ = r := by rw [RCLike.norm_ofReal, abs_of_pos hr]
     have hr_ne : (↑r : 𝕜) ≠ 0 := by exact_mod_cast hr.ne'
     have hxV := hab (↑r : 𝕜) (by rw [hr_norm]) hx
     rw [Set.mem_smul_set_iff_inv_smul_mem₀ hr_ne] at hxV
     simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right] at hxV
-    have hfsmul : f ((↑r : 𝕜)⁻¹ • x) = (↑r : 𝕜)⁻¹ • f x := map_smul f (↑r : 𝕜)⁻¹ (x : F)
+    have hfsmul : f ((↑r : 𝕜)⁻¹ • x) = (↑r : 𝕜)⁻¹ • f x := map_smul f (↑r : 𝕜)⁻¹ (x : E)
     rw [hfsmul, norm_smul, norm_inv, hr_norm] at hxV
     linarith [inv_mul_lt_iff₀ hr |>.mp hxV]
-  · -- Backward: each eval bounded → vonN bounded
-    intro h V hV
-    -- V ∈ nhds 0 in the weak topology (= induced topology from pi)
-    let φ : WeakSpace 𝕜 F → (StrongDual 𝕜 F → 𝕜) := fun x f => f x
+  · intro h V hV
+    let φ : WeakSpace 𝕜 E → (StrongDual 𝕜 E → 𝕜) := fun x f => f x
     have hφ0 : φ 0 = 0 := funext fun f => map_zero f
-    -- nhds 0 in WeakSpace = comap φ (nhds 0) in pi
-    rw [show 𝓝 (0 : WeakSpace 𝕜 F) = Filter.comap φ (𝓝 0) from
+    rw [show 𝓝 (0 : WeakSpace 𝕜 E) = Filter.comap φ (𝓝 0) from
       hφ0 ▸ nhds_induced φ 0, Filter.mem_comap] at hV
     obtain ⟨U, hU, hUV⟩ := hV
     rw [nhds_pi, Filter.mem_pi] at hU
     obtain ⟨I, hI, t, ht, htU⟩ := hU
-    -- Suffices to show the smaller preimage absorbs s
     apply Absorbs.mono_left _ (Set.Subset.trans (Set.preimage_mono htU) hUV)
-    -- Convert preimage of Set.pi to biInter of preimages
-    have hpi : φ ⁻¹' I.pi t = ⋂ f ∈ I, (fun (x : WeakSpace 𝕜 F) => f x) ⁻¹' t f := by
+    have hpi : φ ⁻¹' I.pi t = ⋂ f ∈ I, (fun (x : WeakSpace 𝕜 E) => f x) ⁻¹' t f := by
       ext x; simp [Set.mem_pi, φ]
     rw [hpi, hI.absorbs_biInter]
     intro f hf
-    -- Show each preimage absorbs s via the image being vonN bounded
     obtain ⟨r, hr⟩ := h f
-    have h_vonN : Bornology.IsVonNBounded 𝕜 ((fun x : WeakSpace 𝕜 F => f x) '' s) :=
+    have h_vonN : Bornology.IsVonNBounded 𝕜 ((fun x : WeakSpace 𝕜 E => f x) '' s) :=
       NormedSpace.image_isVonNBounded_iff (𝕜 := 𝕜).mpr ⟨r, hr⟩
     have h_abs := h_vonN (ht f)
-    -- Convert: Absorbs 𝕜 (t f) (f '' s) → Absorbs 𝕜 (f⁻¹' t f) s
     rw [absorbs_iff_eventually_cobounded_mapsTo] at h_abs ⊢
     exact h_abs.mono fun c hc x hx => by
       simp only [Set.mem_preimage]
-      have : f (c⁻¹ • x) = c⁻¹ • f x := map_smul f c⁻¹ (x : F)
+      have : f (c⁻¹ • x) = c⁻¹ • f x := map_smul f c⁻¹ (x : E)
       rw [this]
       exact hc (Set.mem_image_of_mem _ hx)
 
 /-- The norm bornology and the weak von Neumann bornology coincide.
 This is a consequence of the Uniform Boundedness Principle applied to the
-image of F in its double dual. -/
-theorem isBounded_iff_isVonNBounded {s : Set (WeakSpace 𝕜 F)} :
+image of E in its double dual. -/
+theorem isBounded_iff_isVonNBounded {s : Set (WeakSpace 𝕜 E)} :
     IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s := by
   constructor
-  · -- Forward: norm bounded → vonN bounded in weak topology
-    intro h
+  · intro h
     rw [isVonNBounded_iff_forall_eval_bounded]
     intro f
-    -- Extract a norm bound from IsBounded (the bornology on WeakSpace is the norm bornology)
-    obtain ⟨C, hC⟩ := (isBounded_iff_forall_norm_le (E := F)).mp h
+    obtain ⟨C, hC⟩ := (isBounded_iff_forall_norm_le (E := E)).mp h
     exact ⟨‖f‖ * C, fun x hx => (f.le_opNorm x).trans (by gcongr; exact hC x hx)⟩
-  · -- Backward: vonN bounded in weak → norm bounded (via Banach-Steinhaus)
-    intro h_vN
+  · intro h_vN
     rw [isVonNBounded_iff_forall_eval_bounded] at h_vN
-    -- View elements of s as functionals on the dual via inclusionInDoubleDual
-    -- Pointwise boundedness: for each f : StrongDual 𝕜 F, ‖(inclusionInDoubleDual x) f‖ ≤ r
-    have h_ptwise : ∀ f : StrongDual 𝕜 F, ∃ C, ∀ x : (toWeakSpace 𝕜 F ⁻¹' s),
-        ‖NormedSpace.inclusionInDoubleDual 𝕜 F x f‖ ≤ C := by
+    have h_ptwise : ∀ f : StrongDual 𝕜 E, ∃ C, ∀ x : (toWeakSpace 𝕜 E ⁻¹' s),
+        ‖NormedSpace.inclusionInDoubleDual 𝕜 E x f‖ ≤ C := by
       intro f
       obtain ⟨r, hr⟩ := h_vN f
       exact ⟨r, fun ⟨x, hx⟩ => by simp only [NormedSpace.dual_def]; exact hr x hx⟩
-    -- Banach-Steinhaus: uniform bound on operator norms
     obtain ⟨C, hC⟩ := banach_steinhaus h_ptwise
-    -- Since inclusionInDoubleDualLi is an isometry, ‖x‖ = ‖inclusionInDoubleDual x‖ ≤ C
-    suffices @IsBounded F _ s from this
+    suffices @IsBounded E _ s from this
     rw [isBounded_iff_forall_norm_le]
     exact ⟨C, fun x hx => by
       rw [← (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map x]

From f785f4f725c2b0702d199e129817f83d8041ca8a Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:00:18 +0100
Subject: [PATCH 09/10] refactor using seminorms

---
 Mathlib/Analysis/Normed/Module/WeakSpace.lean | 112 ++++++++----------
 1 file changed, 51 insertions(+), 61 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakSpace.lean b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
index 98be07c3a49925..2506aa96a0061f 100644
--- a/Mathlib/Analysis/Normed/Module/WeakSpace.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakSpace.lean
@@ -7,6 +7,7 @@ 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
 
 /-!
@@ -14,11 +15,42 @@ import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 
 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
@@ -49,6 +81,13 @@ 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
@@ -64,73 +103,24 @@ instance instT2Space : T2Space (WeakSpace 𝕜 E) :=
     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
 
-/-- A set in `WeakSpace 𝕜 E` is von Neumann bounded iff it is bounded under
-every continuous linear functional. -/
-theorem isVonNBounded_iff_forall_eval_bounded {s : Set (WeakSpace 𝕜 E)} :
-    Bornology.IsVonNBounded 𝕜 s ↔ ∀ f : StrongDual 𝕜 E, ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
-  constructor
-  · intro hs f
-    have hcont : Continuous fun x : WeakSpace 𝕜 E => f x := WeakBilin.eval_continuous _ f
-    have hmem : (fun x : WeakSpace 𝕜 E => f x) ⁻¹' Metric.ball 0 1 ∈ 𝓝 (0 : WeakSpace 𝕜 E) :=
-      hcont.continuousAt.preimage_mem_nhds (by
-        change Metric.ball 0 1 ∈ 𝓝 ((f : E →L[𝕜] 𝕜) 0)
-        rw [map_zero]; exact Metric.ball_mem_nhds 0 one_pos)
-    obtain ⟨r, hr, hab⟩ := (hs hmem).exists_pos
-    refine ⟨r, fun x hx => ?_⟩
-    have hr_norm : ‖(↑r : 𝕜)‖ = r := by rw [RCLike.norm_ofReal, abs_of_pos hr]
-    have hr_ne : (↑r : 𝕜) ≠ 0 := by exact_mod_cast hr.ne'
-    have hxV := hab (↑r : 𝕜) (by rw [hr_norm]) hx
-    rw [Set.mem_smul_set_iff_inv_smul_mem₀ hr_ne] at hxV
-    simp only [Set.mem_preimage, Metric.mem_ball, dist_zero_right] at hxV
-    have hfsmul : f ((↑r : 𝕜)⁻¹ • x) = (↑r : 𝕜)⁻¹ • f x := map_smul f (↑r : 𝕜)⁻¹ (x : E)
-    rw [hfsmul, norm_smul, norm_inv, hr_norm] at hxV
-    linarith [inv_mul_lt_iff₀ hr |>.mp hxV]
-  · intro h V hV
-    let φ : WeakSpace 𝕜 E → (StrongDual 𝕜 E → 𝕜) := fun x f => f x
-    have hφ0 : φ 0 = 0 := funext fun f => map_zero f
-    rw [show 𝓝 (0 : WeakSpace 𝕜 E) = Filter.comap φ (𝓝 0) from
-      hφ0 ▸ nhds_induced φ 0, Filter.mem_comap] at hV
-    obtain ⟨U, hU, hUV⟩ := hV
-    rw [nhds_pi, Filter.mem_pi] at hU
-    obtain ⟨I, hI, t, ht, htU⟩ := hU
-    apply Absorbs.mono_left _ (Set.Subset.trans (Set.preimage_mono htU) hUV)
-    have hpi : φ ⁻¹' I.pi t = ⋂ f ∈ I, (fun (x : WeakSpace 𝕜 E) => f x) ⁻¹' t f := by
-      ext x; simp [Set.mem_pi, φ]
-    rw [hpi, hI.absorbs_biInter]
-    intro f hf
-    obtain ⟨r, hr⟩ := h f
-    have h_vonN : Bornology.IsVonNBounded 𝕜 ((fun x : WeakSpace 𝕜 E => f x) '' s) :=
-      NormedSpace.image_isVonNBounded_iff (𝕜 := 𝕜).mpr ⟨r, hr⟩
-    have h_abs := h_vonN (ht f)
-    rw [absorbs_iff_eventually_cobounded_mapsTo] at h_abs ⊢
-    exact h_abs.mono fun c hc x hx => by
-      simp only [Set.mem_preimage]
-      have : f (c⁻¹ • x) = c⁻¹ • f x := map_smul f c⁻¹ (x : E)
-      rw [this]
-      exact hc (Set.mem_image_of_mem _ hx)
-
-/-- The norm bornology and the weak von Neumann bornology coincide.
-This is a consequence of the Uniform Boundedness Principle applied to the
-image of E in its double dual. -/
+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
-  · intro h
-    rw [isVonNBounded_iff_forall_eval_bounded]
-    intro f
-    obtain ⟨C, hC⟩ := (isBounded_iff_forall_norm_le (E := E)).mp h
-    exact ⟨‖f‖ * C, fun x hx => (f.le_opNorm x).trans (by gcongr; exact hC x hx)⟩
+  · exact fun h => ((NormedSpace.isVonNBounded_iff (E := E) (𝕜 := 𝕜)).mpr h).of_topologicalSpace_le
+      norm_topology_le_weakSpace_topology
   · intro h_vN
-    rw [isVonNBounded_iff_forall_eval_bounded] at h_vN
-    have h_ptwise : ∀ f : StrongDual 𝕜 E, ∃ C, ∀ x : (toWeakSpace 𝕜 E ⁻¹' s),
-        ‖NormedSpace.inclusionInDoubleDual 𝕜 E x f‖ ≤ C := by
-      intro f
-      obtain ⟨r, hr⟩ := h_vN f
-      exact ⟨r, fun ⟨x, hx⟩ => by simp only [NormedSpace.dual_def]; exact hr x hx⟩
-    obtain ⟨C, hC⟩ := banach_steinhaus h_ptwise
+    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
+    exact ⟨C, fun x hx ↦ by
       rw [← (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map x]
       exact hC ⟨x, hx⟩⟩
 

From f35bacec010fd41e1e6161d112ee064c3a3cf5d5 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 12:28:52 +0100
Subject: [PATCH 10/10] Add WeakSpace to Mathlib.lean

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 47f0e25aeafcd3..74f650fde894f2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -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