From 266494fca0c9b242802b9abaec2d812fc7c0e43b Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 26 May 2026 10:06:41 +0000
Subject: [PATCH 01/43] start with ultratrong def

---
 LeanOA/Predual.lean         | 14 +++++++
 LeanOA/Ultrastrong.lean     | 79 +++++++++++++++++++++++++++++++++++++
 LeanOA/Ultraweak/Basic.lean |  9 +----
 3 files changed, 94 insertions(+), 8 deletions(-)
 create mode 100644 LeanOA/Predual.lean
 create mode 100644 LeanOA/Ultrastrong.lean

diff --git a/LeanOA/Predual.lean b/LeanOA/Predual.lean
new file mode 100644
index 00000000..3a0dcfa4
--- /dev/null
+++ b/LeanOA/Predual.lean
@@ -0,0 +1,14 @@
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.Analysis.Normed.Operator.Basic
+
+public section
+
+/-- A class which encodes a specified isometric linear isomorpism between `M`
+and the strong dual of `P`, so that we may treat `P` as a predual of `M`. -/
+class Predual (𝕜 M P : Type*) [RCLike 𝕜]
+    [NormedAddCommGroup M] [NormedAddCommGroup P]
+    [NormedSpace 𝕜 M] [NormedSpace 𝕜 P] where
+  /-- A linear isometric equivalence between `M` and the dual of its predual `P`. -/
+  equivDual : M ≃ₗᵢ[𝕜] StrongDual 𝕜 P
diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
new file mode 100644
index 00000000..d762b861
--- /dev/null
+++ b/LeanOA/Ultrastrong.lean
@@ -0,0 +1,79 @@
+module
+
+public import LeanOA.Predual
+
+public section
+
+@[expose]
+def Ultrastrong (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
+    [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
+
+variable {𝕜 M P : Type*} [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
+  [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P]
+
+variable (𝕜 M P) in
+/-- The canonical map from `M` to `Ultrastrong 𝕜 M P`. -/
+@[expose] def toUltrastrong (x : M) : Ultrastrong 𝕜 M P := x
+
+/-- The canonical map from `Ultrastrong 𝕜 M P` to `M`. -/
+@[expose] def Ultrastrong.ofUltrastrong (x : Ultrastrong 𝕜 M P) : M := x
+
+namespace Ultrastrong
+
+@[simp] lemma toUltrastrong_ofUltrastrong (x : Ultrastrong 𝕜 M P) :
+    toUltrastrong 𝕜 M P x.ofUltrastrong = x := rfl
+
+@[simp] lemma ofUltrastrong_toUltrastrong (x : M) :
+    (toUltrastrong 𝕜 M P x).ofUltrastrong = x := rfl
+
+variable (𝕜 M P) in
+/-- The canonical equivalence between `Ultrastrong 𝕜 M P` and `M`. -/
+@[expose, simps] def equiv : Ultrastrong 𝕜 M P ≃ M where
+  toFun := ofUltrastrong
+  invFun := toUltrastrong 𝕜 M P
+
+instance : AddCommGroup (Ultrastrong 𝕜 M P) := equiv 𝕜 M P |>.addCommGroup
+instance : Module 𝕜 (Ultrastrong 𝕜 M P) := equiv 𝕜 M P |>.module 𝕜
+
+@[simp] lemma toUltrastrong_add (x y : M) :
+    toUltrastrong 𝕜 M P (x + y) = toUltrastrong 𝕜 M P x + toUltrastrong 𝕜 M P y := rfl
+
+@[simp] lemma ofUltrastrong_add (x y : Ultrastrong 𝕜 M P) :
+    (x + y).ofUltrastrong = x.ofUltrastrong + y.ofUltrastrong := rfl
+
+@[simp] lemma toUltrastrong_smul (a : 𝕜) (x : M) :
+    toUltrastrong 𝕜 M P (a • x) = a • toUltrastrong 𝕜 M P x := rfl
+
+@[simp] lemma ofUltrastrong_smul (a : 𝕜) (x : Ultrastrong 𝕜 M P) :
+    (a • x).ofUltrastrong = a • x.ofUltrastrong := rfl
+
+@[simp] lemma toUltrastrong_zero : toUltrastrong 𝕜 M P (0 : M) = 0 := rfl
+@[simp] lemma ofUltrastrong_zero : (0 : Ultrastrong 𝕜 M P).ofUltrastrong = 0 := rfl
+
+@[simp] lemma toUltrastrong_neg (x : M) :
+    toUltrastrong 𝕜 M P (-x) = -toUltrastrong 𝕜 M P x := rfl
+
+@[simp] lemma ofUltrastrong_neg (x : Ultrastrong 𝕜 M P) :
+    (-x).ofUltrastrong = -x.ofUltrastrong := rfl
+
+@[simp] lemma toUltrastrong_sub (x y : M) :
+    toUltrastrong 𝕜 M P (x - y) = toUltrastrong 𝕜 M P x - toUltrastrong 𝕜 M P y := rfl
+
+@[simp] lemma ofUltrastrong_sub (x y : Ultrastrong 𝕜 M P) :
+    (x - y).ofUltrastrong = x.ofUltrastrong - y.ofUltrastrong := rfl
+
+@[simp] lemma toUltrastrong_inj {x y : M} :
+    toUltrastrong 𝕜 M P x = toUltrastrong 𝕜 M P y ↔ x = y :=
+  equiv 𝕜 M P |>.symm.injective.eq_iff
+
+@[simp] lemma ofUltrastrong_inj {x y : Ultrastrong 𝕜 M P} :
+    x.ofUltrastrong = y.ofUltrastrong ↔ x = y :=
+  equiv 𝕜 M P |>.injective.eq_iff
+
+@[simp] lemma toUltrastrong_eq_zero {x : M} : toUltrastrong 𝕜 M P x = 0 ↔ x = 0 :=
+  toUltrastrong_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ toUltrastrong_inj
+
+@[simp] lemma ofUltrastrong_eq_zero {x : Ultrastrong 𝕜 M P} : x.ofUltrastrong = 0 ↔ x = 0 :=
+  ofUltrastrong_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ ofUltrastrong_inj
+
+end Ultrastrong
diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index d82aac05..507c44c7 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -4,17 +4,10 @@ public import Mathlib.Analysis.CStarAlgebra.Classes
 public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import LeanOA.Mathlib.Analysis.RCLike.Extend
+public import LeanOA.Predual
 
 @[expose] public section
 
-/-- A class which encodes a specified isometric linear isomorpism between `M`
-and the strong dual of `P`, so that we may treat `P` as a predual of `M`. -/
-class Predual (𝕜 M P : Type*) [RCLike 𝕜]
-    [NormedAddCommGroup M] [NormedAddCommGroup P]
-    [NormedSpace 𝕜 M] [NormedSpace 𝕜 P] where
-  /-- A linear isometric equivalence between `M` and the dual of its predual `P`. -/
-  equivDual : M ≃ₗᵢ[𝕜] StrongDual 𝕜 P
-
 
 set_option linter.unusedVariables false in
 /-- A type synonym of `M` equipped with the *ultraweak topology* (also known as the

From 32be630d1741535ce962917743b84076e6ddccab Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 26 May 2026 10:08:12 +0000
Subject: [PATCH 02/43] mk_all

---
 LeanOA.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/LeanOA.lean b/LeanOA.lean
index a6609509..98b40138 100644
--- a/LeanOA.lean
+++ b/LeanOA.lean
@@ -36,8 +36,10 @@ public import LeanOA.Mathlib.Topology.ContinuousMap.ContinuousMapZero
 public import LeanOA.Mathlib.Topology.Order.LeftRightNhds
 public import LeanOA.Notation
 public import LeanOA.PositiveContinuousLinearMap
+public import LeanOA.Predual
 public import LeanOA.TendstoZero.Defs
 public import LeanOA.TendstoZero.StrongDual
+public import LeanOA.Ultrastrong
 public import LeanOA.Ultraweak.Basic
 public import LeanOA.Ultraweak.Bornology
 public import LeanOA.Ultraweak.ContinuousFunctionalCalculus

From 3722e6ce1fdcc760e162d95725f192e0e3416485 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Mon, 1 Jun 2026 10:57:00 -0400
Subject: [PATCH 03/43] notation and a trivial linear equivalence.

---
 LeanOA/Ultrastrong.lean     | 56 ++++++++++++++++++++++++++-----------
 LeanOA/Ultraweak/Basic.lean |  4 +--
 2 files changed, 42 insertions(+), 18 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index d762b861..ff3a22fd 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -4,76 +4,100 @@ public import LeanOA.Predual
 
 public section
 
+
+/-- Type synonym for `M` with the ultrastrong topology. -/
 @[expose]
 def Ultrastrong (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
 
+@[inherit_doc]
+scoped[Ultrastrong] notation "s("M", " P")_" 𝕜:max => Ultrastrong 𝕜 M P
+@[inherit_doc]
+scoped[Ultrastrong] notation "s("M", " P")" => Ultrastrong ℂ M P
+
+/-! ## Linear structure -/
+
 variable {𝕜 M P : Type*} [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
   [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P]
 
+open Ultrastrong
+
 variable (𝕜 M P) in
-/-- The canonical map from `M` to `Ultrastrong 𝕜 M P`. -/
-@[expose] def toUltrastrong (x : M) : Ultrastrong 𝕜 M P := x
+/-- The canonical map from `M` to `s(M, P)_𝕜`. -/
+@[expose] def toUltrastrong (x : M) : s(M, P)_𝕜 := x
 
-/-- The canonical map from `Ultrastrong 𝕜 M P` to `M`. -/
-@[expose] def Ultrastrong.ofUltrastrong (x : Ultrastrong 𝕜 M P) : M := x
+/-- The canonical map from `s(M, P)_𝕜` to `M`. -/
+@[expose] def Ultrastrong.ofUltrastrong (x : s(M, P)_𝕜) : M := x
 
 namespace Ultrastrong
 
-@[simp] lemma toUltrastrong_ofUltrastrong (x : Ultrastrong 𝕜 M P) :
+@[simp] lemma toUltrastrong_ofUltrastrong (x : s(M, P)_𝕜) :
     toUltrastrong 𝕜 M P x.ofUltrastrong = x := rfl
 
 @[simp] lemma ofUltrastrong_toUltrastrong (x : M) :
     (toUltrastrong 𝕜 M P x).ofUltrastrong = x := rfl
 
 variable (𝕜 M P) in
-/-- The canonical equivalence between `Ultrastrong 𝕜 M P` and `M`. -/
-@[expose, simps] def equiv : Ultrastrong 𝕜 M P ≃ M where
+/-- The canonical equivalence between `s(M, P)_𝕜` and `M`. -/
+@[expose, simps] def equiv : s(M, P)_𝕜 ≃ M where
   toFun := ofUltrastrong
   invFun := toUltrastrong 𝕜 M P
 
-instance : AddCommGroup (Ultrastrong 𝕜 M P) := equiv 𝕜 M P |>.addCommGroup
-instance : Module 𝕜 (Ultrastrong 𝕜 M P) := equiv 𝕜 M P |>.module 𝕜
+instance : AddCommGroup (s(M, P)_𝕜) := equiv 𝕜 M P |>.addCommGroup
+instance : Module 𝕜 (s(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
 
 @[simp] lemma toUltrastrong_add (x y : M) :
     toUltrastrong 𝕜 M P (x + y) = toUltrastrong 𝕜 M P x + toUltrastrong 𝕜 M P y := rfl
 
-@[simp] lemma ofUltrastrong_add (x y : Ultrastrong 𝕜 M P) :
+@[simp] lemma ofUltrastrong_add (x y : s(M, P)_𝕜) :
     (x + y).ofUltrastrong = x.ofUltrastrong + y.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_smul (a : 𝕜) (x : M) :
     toUltrastrong 𝕜 M P (a • x) = a • toUltrastrong 𝕜 M P x := rfl
 
-@[simp] lemma ofUltrastrong_smul (a : 𝕜) (x : Ultrastrong 𝕜 M P) :
+@[simp] lemma ofUltrastrong_smul (a : 𝕜) (x : s(M, P)_𝕜) :
     (a • x).ofUltrastrong = a • x.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_zero : toUltrastrong 𝕜 M P (0 : M) = 0 := rfl
-@[simp] lemma ofUltrastrong_zero : (0 : Ultrastrong 𝕜 M P).ofUltrastrong = 0 := rfl
+@[simp] lemma ofUltrastrong_zero : (0 : s(M, P)_𝕜).ofUltrastrong = 0 := rfl
 
 @[simp] lemma toUltrastrong_neg (x : M) :
     toUltrastrong 𝕜 M P (-x) = -toUltrastrong 𝕜 M P x := rfl
 
-@[simp] lemma ofUltrastrong_neg (x : Ultrastrong 𝕜 M P) :
+@[simp] lemma ofUltrastrong_neg (x : s(M, P)_𝕜) :
     (-x).ofUltrastrong = -x.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_sub (x y : M) :
     toUltrastrong 𝕜 M P (x - y) = toUltrastrong 𝕜 M P x - toUltrastrong 𝕜 M P y := rfl
 
-@[simp] lemma ofUltrastrong_sub (x y : Ultrastrong 𝕜 M P) :
+@[simp] lemma ofUltrastrong_sub (x y : s(M, P)_𝕜) :
     (x - y).ofUltrastrong = x.ofUltrastrong - y.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_inj {x y : M} :
     toUltrastrong 𝕜 M P x = toUltrastrong 𝕜 M P y ↔ x = y :=
   equiv 𝕜 M P |>.symm.injective.eq_iff
 
-@[simp] lemma ofUltrastrong_inj {x y : Ultrastrong 𝕜 M P} :
+@[simp] lemma ofUltrastrong_inj {x y : s(M, P)_𝕜} :
     x.ofUltrastrong = y.ofUltrastrong ↔ x = y :=
   equiv 𝕜 M P |>.injective.eq_iff
 
 @[simp] lemma toUltrastrong_eq_zero {x : M} : toUltrastrong 𝕜 M P x = 0 ↔ x = 0 :=
   toUltrastrong_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ toUltrastrong_inj
 
-@[simp] lemma ofUltrastrong_eq_zero {x : Ultrastrong 𝕜 M P} : x.ofUltrastrong = 0 ↔ x = 0 :=
+@[simp] lemma ofUltrastrong_eq_zero {x : s(M, P)_𝕜} : x.ofUltrastrong = 0 ↔ x = 0 :=
   ofUltrastrong_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ ofUltrastrong_inj
 
+/-! ## Equivalences -/
+
+variable (𝕜 M P) in
+/-- The canonical linear equivalence between `s(M, P)_𝕜` and `M`. -/
+@[expose, simps]
+def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
+  toFun := ofUltrastrong
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  invFun := toUltrastrong 𝕜 M P
+  left_inv _ := rfl
+  right_inv _ := rfl
+
 end Ultrastrong
diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index 507c44c7..efe9dc04 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -22,9 +22,9 @@ abbrev Ultraweak (𝕜 M P : Type*) [RCLike 𝕜] [NormedAddCommGroup M] [Normed
   WeakBilin <| topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap)
 
 @[inherit_doc]
-scoped[Ultraweak] notation "σ("M ", " P")_" 𝕜:max => Ultraweak 𝕜 M P
+scoped[Ultraweak] notation "σ("M", " P")_" 𝕜:max => Ultraweak 𝕜 M P
 @[inherit_doc]
-scoped[Ultraweak] notation "σ("M ", " P")" => Ultraweak ℂ M P
+scoped[Ultraweak] notation "σ("M", " P")" => Ultraweak ℂ M P
 
 /-! ## Linear structure -/
 

From 61ee43f46062ed77543434d3903d7a9c4932862f Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 2 Jun 2026 09:22:11 -0400
Subject: [PATCH 04/43] applied `toEquiv` suggestion

---
 LeanOA/Ultrastrong.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index ff3a22fd..eba9e2ab 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -93,11 +93,8 @@ variable (𝕜 M P) in
 /-- The canonical linear equivalence between `s(M, P)_𝕜` and `M`. -/
 @[expose, simps]
 def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
-  toFun := ofUltrastrong
+  toEquiv := equiv 𝕜 M P
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
-  invFun := toUltrastrong 𝕜 M P
-  left_inv _ := rfl
-  right_inv _ := rfl
 
 end Ultrastrong

From ea93ec6da30555bc1be1517e4e175bce6186c1d3 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 10:42:40 -0400
Subject: [PATCH 05/43] Seminorm Family is now there (can be overwritten by
 Monica when she gets the new computer.)

---
 .../CStarAlgebra/PositiveLinearFunctional.lean   |  4 ++++
 LeanOA/Ultrastrong.lean                          | 16 ++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean b/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
index fa3b82e6..bf780473 100644
--- a/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
+++ b/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
@@ -61,9 +61,13 @@ noncomputable abbrev preGNS'preInnerProdSpace : PreInnerProductSpace.Core ℂ f.
 
 noncomputable instance : SeminormedAddCommGroup f.PreGNS' :=
   InnerProductSpace.Core.toSeminormedAddCommGroup (c := f.preGNS'preInnerProdSpace)
+
 noncomputable instance : InnerProductSpace ℂ f.PreGNS' :=
   InnerProductSpace.ofCore f.preGNS'preInnerProdSpace
 
+noncomputable instance : SeminormedSpace.Core ℂ f.PreGNS' :=
+  InnerProductSpace.Core.toSeminormedSpaceCore (c := f.preGNS'preInnerProdSpace)
+
 lemma preGNS'_inner_def (a b : f.PreGNS') :
     ⟪a, b⟫_ℂ = f (star (f.ofPreGNS' a) * f.ofPreGNS' b) := rfl
 
diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index eba9e2ab..639abe0b 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -1,6 +1,11 @@
 module
 
+--public import Mathlib
 public import LeanOA.Predual
+public import LeanOA.Ultraweak.Basic
+public import LeanOA.CStarAlgebra.PositiveLinearFunctional
+public import Mathlib.Analysis.LocallyConvex.WithSeminorms
+public import Mathlib.Analysis.Normed.Module.TransferInstance
 
 public section
 
@@ -97,4 +102,15 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
+variable {𝕜 M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
+variable [NormedAlgebra ℂ M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P]
+variable [StarModule ℂ M] [SelfAdjointDecompose M]
+
+open ComplexOrder PositiveLinearMap
+
+noncomputable def SeminormFamily : SeminormFamily ℂ
+  (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
+  fun f ↦ Seminorm.comp (normSeminorm ℂ (f.val.PreGNS'))
+      ((Ultrastrong.linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
+
 end Ultrastrong

From 80952b3b98bf41f6af90408acc156d1d8ef48dc0 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 10:53:18 -0400
Subject: [PATCH 06/43] topological space instance from ModuleFilterBasis. No
 Uniformity yet...

---
 LeanOA/Ultrastrong.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 639abe0b..a2aff0a9 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -64,6 +64,7 @@ instance : Module 𝕜 (s(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
     (a • x).ofUltrastrong = a • x.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_zero : toUltrastrong 𝕜 M P (0 : M) = 0 := rfl
+
 @[simp] lemma ofUltrastrong_zero : (0 : s(M, P)_𝕜).ofUltrastrong = 0 := rfl
 
 @[simp] lemma toUltrastrong_neg (x : M) :
@@ -102,15 +103,21 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
+/-! ## The Topology -/
+
 variable {𝕜 M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
 variable [NormedAlgebra ℂ M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P]
 variable [StarModule ℂ M] [SelfAdjointDecompose M]
 
 open ComplexOrder PositiveLinearMap
 
-noncomputable def SeminormFamily : SeminormFamily ℂ
+noncomputable def seminormFamily : SeminormFamily ℂ
   (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
   fun f ↦ Seminorm.comp (normSeminorm ℂ (f.val.PreGNS'))
       ((Ultrastrong.linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
 
+noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
+
+noncomputable abbrev TopologicalSpace : TopologicalSpace s(M, P) := FilterBasis.topology'
+
 end Ultrastrong

From 0c6926e2131576ab2b64ec16e5f8e9bba57ee3f8 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 10:54:54 -0400
Subject: [PATCH 07/43] This can be an instance, I guess, since we are working
 over that canonical family...

---
 LeanOA/Ultrastrong.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index a2aff0a9..7fb198de 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -118,6 +118,6 @@ noncomputable def seminormFamily : SeminormFamily ℂ
 
 noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
 
-noncomputable abbrev TopologicalSpace : TopologicalSpace s(M, P) := FilterBasis.topology'
+noncomputable instance TopologicalSpace : TopologicalSpace s(M, P) := FilterBasis.topology'
 
 end Ultrastrong

From 9b0ba1cf3c842ce3f37a3c7928daf41aa5062779 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 10:55:25 -0400
Subject: [PATCH 08/43] Shoot. I don't need to name the instance, though!

---
 LeanOA/Ultrastrong.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 7fb198de..190b6611 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -118,6 +118,6 @@ noncomputable def seminormFamily : SeminormFamily ℂ
 
 noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
 
-noncomputable instance TopologicalSpace : TopologicalSpace s(M, P) := FilterBasis.topology'
+noncomputable instance : TopologicalSpace s(M, P) := FilterBasis.topology'
 
 end Ultrastrong

From 4fceb9f64146312916fc86f3f502a8ce45a7813d Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 14:07:44 -0400
Subject: [PATCH 09/43] WithSeminorms...trivial def.

---
 LeanOA/Ultrastrong.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 190b6611..a5424674 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -120,4 +120,8 @@ noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.
 
 noncomputable instance : TopologicalSpace s(M, P) := FilterBasis.topology'
 
+/-- This is probably a stupid definition, but in case we want `WithSeminorms` ever. -/
+def withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
+  { topology_eq_withSeminorms := rfl }
+
 end Ultrastrong

From 8bea6eebbe63b5ca2e86fc3fb55fd6fb9d17382c Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 3 Jun 2026 14:54:25 -0400
Subject: [PATCH 10/43] Small change

---
 LeanOA/Ultrastrong.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index a5424674..14d7586b 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -120,7 +120,7 @@ noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.
 
 noncomputable instance : TopologicalSpace s(M, P) := FilterBasis.topology'
 
-/-- This is probably a stupid definition, but in case we want `WithSeminorms` ever. -/
+/-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
 def withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 

From 5f7f2f94d05568455aed0b3036b8460d9cf1ebb4 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:04:10 +0100
Subject: [PATCH 11/43] some cleanup

---
 LeanOA/Ultrastrong.lean | 25 ++++++++-----------------
 1 file changed, 8 insertions(+), 17 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 14d7586b..2f41f31c 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -1,6 +1,5 @@
 module
 
---public import Mathlib
 public import LeanOA.Predual
 public import LeanOA.Ultraweak.Basic
 public import LeanOA.CStarAlgebra.PositiveLinearFunctional
@@ -9,7 +8,6 @@ public import Mathlib.Analysis.Normed.Module.TransferInstance
 
 public section
 
-
 /-- Type synonym for `M` with the ultrastrong topology. -/
 @[expose]
 def Ultrastrong (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
@@ -64,14 +62,9 @@ instance : Module 𝕜 (s(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
     (a • x).ofUltrastrong = a • x.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_zero : toUltrastrong 𝕜 M P (0 : M) = 0 := rfl
-
 @[simp] lemma ofUltrastrong_zero : (0 : s(M, P)_𝕜).ofUltrastrong = 0 := rfl
-
-@[simp] lemma toUltrastrong_neg (x : M) :
-    toUltrastrong 𝕜 M P (-x) = -toUltrastrong 𝕜 M P x := rfl
-
-@[simp] lemma ofUltrastrong_neg (x : s(M, P)_𝕜) :
-    (-x).ofUltrastrong = -x.ofUltrastrong := rfl
+@[simp] lemma toUltrastrong_neg (x : M) : toUltrastrong 𝕜 M P (-x) = -toUltrastrong 𝕜 M P x := rfl
+@[simp] lemma ofUltrastrong_neg (x : s(M, P)_𝕜) : (-x).ofUltrastrong = -x.ofUltrastrong := rfl
 
 @[simp] lemma toUltrastrong_sub (x y : M) :
     toUltrastrong 𝕜 M P (x - y) = toUltrastrong 𝕜 M P x - toUltrastrong 𝕜 M P y := rfl
@@ -79,12 +72,10 @@ instance : Module 𝕜 (s(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
 @[simp] lemma ofUltrastrong_sub (x y : s(M, P)_𝕜) :
     (x - y).ofUltrastrong = x.ofUltrastrong - y.ofUltrastrong := rfl
 
-@[simp] lemma toUltrastrong_inj {x y : M} :
-    toUltrastrong 𝕜 M P x = toUltrastrong 𝕜 M P y ↔ x = y :=
+@[simp] lemma toUltrastrong_inj {x y : M} : toUltrastrong 𝕜 M P x = toUltrastrong 𝕜 M P y ↔ x = y :=
   equiv 𝕜 M P |>.symm.injective.eq_iff
 
-@[simp] lemma ofUltrastrong_inj {x y : s(M, P)_𝕜} :
-    x.ofUltrastrong = y.ofUltrastrong ↔ x = y :=
+@[simp] lemma ofUltrastrong_inj {x y : s(M, P)_𝕜} : x.ofUltrastrong = y.ofUltrastrong ↔ x = y :=
   equiv 𝕜 M P |>.injective.eq_iff
 
 @[simp] lemma toUltrastrong_eq_zero {x : M} : toUltrastrong 𝕜 M P x = 0 ↔ x = 0 :=
@@ -105,16 +96,16 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
 
 /-! ## The Topology -/
 
-variable {𝕜 M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
+variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
 variable [NormedAlgebra ℂ M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P]
 variable [StarModule ℂ M] [SelfAdjointDecompose M]
 
 open ComplexOrder PositiveLinearMap
 
 noncomputable def seminormFamily : SeminormFamily ℂ
-  (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
-  fun f ↦ Seminorm.comp (normSeminorm ℂ (f.val.PreGNS'))
-      ((Ultrastrong.linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
+    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
+  fun f ↦ (normSeminorm ℂ (f.val.PreGNS')).comp
+    ((linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
 
 noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
 

From e30c4ef03705479a7827ca5adc361cdbb1ce4591 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:05:35 +0100
Subject: [PATCH 12/43] docstrings

---
 LeanOA/Ultrastrong.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 2f41f31c..6936bd30 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -102,14 +102,16 @@ variable [StarModule ℂ M] [SelfAdjointDecompose M]
 
 open ComplexOrder PositiveLinearMap
 
+/-- Seminorm family for the ultrastrong topology. -/
 noncomputable def seminormFamily : SeminormFamily ℂ
     (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
   fun f ↦ (normSeminorm ℂ (f.val.PreGNS')).comp
     ((linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
 
-noncomputable def FilterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
+/-- Filter basis for the seminorm family for the ultrastrong topology. -/
+noncomputable def filterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
 
-noncomputable instance : TopologicalSpace s(M, P) := FilterBasis.topology'
+noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 
 /-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
 def withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=

From 67b2bc212b90b1075f1f0b1fa200aa5edfb0179e Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:18:32 +0100
Subject: [PATCH 13/43] fix

---
 LeanOA/Ultrastrong.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 6936bd30..fc96e5fe 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -8,8 +8,9 @@ public import Mathlib.Analysis.Normed.Module.TransferInstance
 
 public section
 
+set_option linter.unusedVariables false in
 /-- Type synonym for `M` with the ultrastrong topology. -/
-@[expose]
+@[expose, nolint unusedArguments]
 def Ultrastrong (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
 
@@ -114,7 +115,7 @@ noncomputable def filterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.
 noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 
 /-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
-def withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
+lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
 end Ultrastrong

From e7b7ef100d82a07fe9ee4bbab4a182acd129b5bd Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Thu, 4 Jun 2026 16:32:01 +0100
Subject: [PATCH 14/43] remove instance

---
 LeanOA/CStarAlgebra/PositiveLinearFunctional.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean b/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
index bf780473..d1672000 100644
--- a/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
+++ b/LeanOA/CStarAlgebra/PositiveLinearFunctional.lean
@@ -65,9 +65,6 @@ noncomputable instance : SeminormedAddCommGroup f.PreGNS' :=
 noncomputable instance : InnerProductSpace ℂ f.PreGNS' :=
   InnerProductSpace.ofCore f.preGNS'preInnerProdSpace
 
-noncomputable instance : SeminormedSpace.Core ℂ f.PreGNS' :=
-  InnerProductSpace.Core.toSeminormedSpaceCore (c := f.preGNS'preInnerProdSpace)
-
 lemma preGNS'_inner_def (a b : f.PreGNS') :
     ⟪a, b⟫_ℂ = f (star (f.ofPreGNS' a) * f.ofPreGNS' b) := rfl
 

From 48d352b0f535132ed450fca4f71d34213a6c4c88 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Thu, 4 Jun 2026 17:52:28 -0400
Subject: [PATCH 15/43] Ultrastrong star set up

---
 LeanOA/Mathlib/Analysis/UltrastrongStar.lean | 131 +++++++++++++++++++
 1 file changed, 131 insertions(+)
 create mode 100644 LeanOA/Mathlib/Analysis/UltrastrongStar.lean

diff --git a/LeanOA/Mathlib/Analysis/UltrastrongStar.lean b/LeanOA/Mathlib/Analysis/UltrastrongStar.lean
new file mode 100644
index 00000000..e7161138
--- /dev/null
+++ b/LeanOA/Mathlib/Analysis/UltrastrongStar.lean
@@ -0,0 +1,131 @@
+module
+
+public import LeanOA.Predual
+public import LeanOA.Ultraweak.Basic
+public import LeanOA.CStarAlgebra.PositiveLinearFunctional
+public import Mathlib.Analysis.LocallyConvex.WithSeminorms
+public import Mathlib.Analysis.Normed.Module.TransferInstance
+
+public section
+
+set_option linter.unusedVariables false in
+/-- Type synonym for `M` with the ultrastrong-star topology. -/
+@[expose, nolint unusedArguments]
+def UltrastrongStar (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
+    [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
+
+@[inherit_doc]
+scoped[UltrastrongStar] notation "s*("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
+@[inherit_doc]
+scoped[UltrastrongStar] notation "s*("M", " P")" => UltrastrongStar ℂ M P
+
+/-! ## Linear structure -/
+
+variable {𝕜 M P : Type*} [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
+  [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P]
+
+open UltrastrongStar
+
+variable (𝕜 M P) in
+/-- The canonical map from `M` to `s*(M, P)_𝕜`. -/
+@[expose] def toUltrastrongStar (x : M) : s*(M, P)_𝕜 := x
+
+/-- The canonical map from `s*(M, P)_𝕜` to `M`. -/
+@[expose] def UltrastrongStar.ofUltrastrongStar (x : s*(M, P)_𝕜) : M := x
+
+namespace UltrastrongStar
+
+@[simp] lemma toUltrastrongStar_ofUltrastrongStar (x : s*(M, P)_𝕜) :
+    toUltrastrongStar 𝕜 M P x.ofUltrastrongStar = x := rfl
+
+@[simp] lemma ofUltrastrongStar_toUltrastrongStar (x : M) :
+    (toUltrastrongStar 𝕜 M P x).ofUltrastrongStar = x := rfl
+
+variable (𝕜 M P) in
+/-- The canonical equivalence between `s*(M, P)_𝕜` and `M`. -/
+@[expose, simps] def equiv : s*(M, P)_𝕜 ≃ M where
+  toFun := ofUltrastrongStar
+  invFun := toUltrastrongStar 𝕜 M P
+
+instance : AddCommGroup (s*(M, P)_𝕜) := equiv 𝕜 M P |>.addCommGroup
+instance : Module 𝕜 (s*(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
+
+@[simp] lemma toUltrastrongStar_add (x y : M) :
+    toUltrastrongStar 𝕜 M P (x + y) = toUltrastrongStar 𝕜 M P x + toUltrastrongStar 𝕜 M P y := rfl
+
+@[simp] lemma ofUltrastrongStar_add (x y : s*(M, P)_𝕜) :
+    (x + y).ofUltrastrongStar = x.ofUltrastrongStar + y.ofUltrastrongStar := rfl
+
+@[simp] lemma toUltrastrongStar_smul (a : 𝕜) (x : M) :
+    toUltrastrongStar 𝕜 M P (a • x) = a • toUltrastrongStar 𝕜 M P x := rfl
+
+@[simp] lemma ofUltrastrongStar_smul (a : 𝕜) (x : s*(M, P)_𝕜) :
+    (a • x).ofUltrastrongStar = a • x.ofUltrastrongStar := rfl
+
+@[simp] lemma toUltrastrongStar_zero : toUltrastrongStar 𝕜 M P (0 : M) = 0 := rfl
+@[simp] lemma ofUltrastrongStar_zero : (0 : s*(M, P)_𝕜).ofUltrastrongStar = 0 := rfl
+
+@[simp] lemma toUltrastrongStar_neg (x : M) :
+  toUltrastrongStar 𝕜 M P (-x) = -toUltrastrongStar 𝕜 M P x := rfl
+
+@[simp] lemma ofUltrastrongStar_neg (x : s*(M, P)_𝕜) :
+  (-x).ofUltrastrongStar = -x.ofUltrastrongStar := rfl
+
+@[simp] lemma toUltrastrongStar_sub (x y : M) :
+    toUltrastrongStar 𝕜 M P (x - y) = toUltrastrongStar 𝕜 M P x - toUltrastrongStar 𝕜 M P y := rfl
+
+@[simp] lemma ofUltrastrongStar_sub (x y : s*(M, P)_𝕜) :
+    (x - y).ofUltrastrongStar = x.ofUltrastrongStar - y.ofUltrastrongStar := rfl
+
+@[simp] lemma toUltrastrongStar_inj {x y : M} :
+    toUltrastrongStar 𝕜 M P x = toUltrastrongStar 𝕜 M P y ↔ x = y :=
+  equiv 𝕜 M P |>.symm.injective.eq_iff
+
+@[simp] lemma ofUltrastrongStar_inj {x y : s*(M, P)_𝕜} :
+    x.ofUltrastrongStar = y.ofUltrastrongStar ↔ x = y :=
+  equiv 𝕜 M P |>.injective.eq_iff
+
+@[simp] lemma toUltrastrongStar_eq_zero {x : M} : toUltrastrongStar 𝕜 M P x = 0 ↔ x = 0 :=
+  toUltrastrongStar_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ toUltrastrongStar_inj
+
+@[simp] lemma ofUltrastrongStar_eq_zero {x : s*(M, P)_𝕜} : x.ofUltrastrongStar = 0 ↔ x = 0 :=
+  ofUltrastrongStar_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ ofUltrastrongStar_inj
+
+/-! ## Equivalences -/
+
+variable (𝕜 M P) in
+/-- The canonical linear equivalence between `s*(M, P)_𝕜` and `M`. -/
+@[expose, simps]
+def linearEquiv : s*(M, P)_𝕜 ≃ₗ[𝕜] M where
+  toEquiv := equiv 𝕜 M P
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/-! ## The Topology -/
+
+variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
+variable [NormedAlgebra ℂ M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P]
+variable [StarModule ℂ M] [SelfAdjointDecompose M] [NormedStarGroup M]
+
+open ComplexOrder PositiveLinearMap
+
+open Ultraweak in
+/-- Seminorm family for the ultrastrong-star topology. -/
+noncomputable def seminormFamily : SeminormFamily ℂ
+    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2) s*(M, P) :=
+  fun f ↦ if f.2 = 0 then (normSeminorm ℂ (f.1.val.PreGNS')).comp
+    ((linearEquiv ℂ M P).trans f.1.val.toPreGNS').toLinearMap else
+      (normSeminorm ℂ (f.1.val.PreGNS')).comp <|
+        (((linearEquiv ℂ M P).trans <| f.1.val.toPreGNS')).trans
+          (starₗᵢ ℂ (E := M)).toContinuousLinearEquiv.toLinearEquiv |>.toLinearMap
+
+/-- Filter basis for the seminorm family for the ultrastrong-star topology. -/
+noncomputable def filterBasis : ModuleFilterBasis ℂ s*(M, P) := seminormFamily.moduleFilterBasis
+
+noncomputable instance : TopologicalSpace s*(M, P) := filterBasis.topology'
+
+/-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
+lemma withSeminorms : WithSeminorms (E := s*(M, P)) seminormFamily :=
+  { topology_eq_withSeminorms := rfl }
+
+end UltrastrongStar

From f8a494841f8c12f24f2e761da6354f71e97ee5ff Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Thu, 4 Jun 2026 18:07:09 -0400
Subject: [PATCH 16/43] Changed to starLinearEquv.

---
 LeanOA/{Mathlib/Analysis => }/UltrastrongStar.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)
 rename LeanOA/{Mathlib/Analysis => }/UltrastrongStar.lean (97%)

diff --git a/LeanOA/Mathlib/Analysis/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
similarity index 97%
rename from LeanOA/Mathlib/Analysis/UltrastrongStar.lean
rename to LeanOA/UltrastrongStar.lean
index e7161138..0fe0e85a 100644
--- a/LeanOA/Mathlib/Analysis/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -105,7 +105,7 @@ def linearEquiv : s*(M, P)_𝕜 ≃ₗ[𝕜] M where
 
 variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
 variable [NormedAlgebra ℂ M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P]
-variable [StarModule ℂ M] [SelfAdjointDecompose M] [NormedStarGroup M]
+variable [StarModule ℂ M] [SelfAdjointDecompose M]
 
 open ComplexOrder PositiveLinearMap
 
@@ -117,7 +117,7 @@ noncomputable def seminormFamily : SeminormFamily ℂ
     ((linearEquiv ℂ M P).trans f.1.val.toPreGNS').toLinearMap else
       (normSeminorm ℂ (f.1.val.PreGNS')).comp <|
         (((linearEquiv ℂ M P).trans <| f.1.val.toPreGNS')).trans
-          (starₗᵢ ℂ (E := M)).toContinuousLinearEquiv.toLinearEquiv |>.toLinearMap
+          (starLinearEquiv ℂ (A := M)) |>.toLinearMap
 
 /-- Filter basis for the seminorm family for the ultrastrong-star topology. -/
 noncomputable def filterBasis : ModuleFilterBasis ℂ s*(M, P) := seminormFamily.moduleFilterBasis

From 3fdcfb22babf8f2641c87279dd8e093388d23451 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Thu, 4 Jun 2026 18:11:23 -0400
Subject: [PATCH 17/43] A little paren cleanup

---
 LeanOA/UltrastrongStar.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 0fe0e85a..8db03c51 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -113,10 +113,10 @@ open Ultraweak in
 /-- Seminorm family for the ultrastrong-star topology. -/
 noncomputable def seminormFamily : SeminormFamily ℂ
     (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2) s*(M, P) :=
-  fun f ↦ if f.2 = 0 then (normSeminorm ℂ (f.1.val.PreGNS')).comp
-    ((linearEquiv ℂ M P).trans f.1.val.toPreGNS').toLinearMap else
-      (normSeminorm ℂ (f.1.val.PreGNS')).comp <|
-        (((linearEquiv ℂ M P).trans <| f.1.val.toPreGNS')).trans
+  fun f ↦ if f.2 = 0 then normSeminorm ℂ f.1.val.PreGNS' |>.comp
+    (linearEquiv ℂ M P |>.trans f.1.val.toPreGNS').toLinearMap else
+      normSeminorm ℂ f.1.val.PreGNS' |>.comp <|
+        (linearEquiv ℂ M P |>.trans <| f.1.val.toPreGNS').trans
           (starLinearEquiv ℂ (A := M)) |>.toLinearMap
 
 /-- Filter basis for the seminorm family for the ultrastrong-star topology. -/

From 5f242b31ec0fde70615f0af6eeecd1fb26dbb942 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 07:51:09 -0400
Subject: [PATCH 18/43] Fixed the stars.

---
 LeanOA/UltrastrongStar.lean | 49 +++++++++++++++++++------------------
 1 file changed, 25 insertions(+), 24 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 8db03c51..5f43feff 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -15,9 +15,9 @@ def UltrastrongStar (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
 
 @[inherit_doc]
-scoped[UltrastrongStar] notation "s*("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
+scoped[UltrastrongStar] notation "s⋆("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
 @[inherit_doc]
-scoped[UltrastrongStar] notation "s*("M", " P")" => UltrastrongStar ℂ M P
+scoped[UltrastrongStar] notation "s⋆("M", " P")" => UltrastrongStar ℂ M P
 
 /-! ## Linear structure -/
 
@@ -27,76 +27,76 @@ variable {𝕜 M P : Type*} [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlg
 open UltrastrongStar
 
 variable (𝕜 M P) in
-/-- The canonical map from `M` to `s*(M, P)_𝕜`. -/
-@[expose] def toUltrastrongStar (x : M) : s*(M, P)_𝕜 := x
+/-- The canonical map from `M` to `s⋆(M, P)_𝕜`. -/
+@[expose] def toUltrastrongStar (x : M) : s⋆(M, P)_𝕜 := x
 
-/-- The canonical map from `s*(M, P)_𝕜` to `M`. -/
-@[expose] def UltrastrongStar.ofUltrastrongStar (x : s*(M, P)_𝕜) : M := x
+/-- The canonical map from `s⋆(M, P)_𝕜` to `M`. -/
+@[expose] def UltrastrongStar.ofUltrastrongStar (x : s⋆(M, P)_𝕜) : M := x
 
 namespace UltrastrongStar
 
-@[simp] lemma toUltrastrongStar_ofUltrastrongStar (x : s*(M, P)_𝕜) :
+@[simp] lemma toUltrastrongStar_ofUltrastrongStar (x : s⋆(M, P)_𝕜) :
     toUltrastrongStar 𝕜 M P x.ofUltrastrongStar = x := rfl
 
 @[simp] lemma ofUltrastrongStar_toUltrastrongStar (x : M) :
     (toUltrastrongStar 𝕜 M P x).ofUltrastrongStar = x := rfl
 
 variable (𝕜 M P) in
-/-- The canonical equivalence between `s*(M, P)_𝕜` and `M`. -/
-@[expose, simps] def equiv : s*(M, P)_𝕜 ≃ M where
+/-- The canonical equivalence between `s⋆(M, P)_𝕜` and `M`. -/
+@[expose, simps] def equiv : s⋆(M, P)_𝕜 ≃ M where
   toFun := ofUltrastrongStar
   invFun := toUltrastrongStar 𝕜 M P
 
-instance : AddCommGroup (s*(M, P)_𝕜) := equiv 𝕜 M P |>.addCommGroup
-instance : Module 𝕜 (s*(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
+instance : AddCommGroup (s⋆(M, P)_𝕜) := equiv 𝕜 M P |>.addCommGroup
+instance : Module 𝕜 (s⋆(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
 
 @[simp] lemma toUltrastrongStar_add (x y : M) :
     toUltrastrongStar 𝕜 M P (x + y) = toUltrastrongStar 𝕜 M P x + toUltrastrongStar 𝕜 M P y := rfl
 
-@[simp] lemma ofUltrastrongStar_add (x y : s*(M, P)_𝕜) :
+@[simp] lemma ofUltrastrongStar_add (x y : s⋆(M, P)_𝕜) :
     (x + y).ofUltrastrongStar = x.ofUltrastrongStar + y.ofUltrastrongStar := rfl
 
 @[simp] lemma toUltrastrongStar_smul (a : 𝕜) (x : M) :
     toUltrastrongStar 𝕜 M P (a • x) = a • toUltrastrongStar 𝕜 M P x := rfl
 
-@[simp] lemma ofUltrastrongStar_smul (a : 𝕜) (x : s*(M, P)_𝕜) :
+@[simp] lemma ofUltrastrongStar_smul (a : 𝕜) (x : s⋆(M, P)_𝕜) :
     (a • x).ofUltrastrongStar = a • x.ofUltrastrongStar := rfl
 
 @[simp] lemma toUltrastrongStar_zero : toUltrastrongStar 𝕜 M P (0 : M) = 0 := rfl
-@[simp] lemma ofUltrastrongStar_zero : (0 : s*(M, P)_𝕜).ofUltrastrongStar = 0 := rfl
+@[simp] lemma ofUltrastrongStar_zero : (0 : s⋆(M, P)_𝕜).ofUltrastrongStar = 0 := rfl
 
 @[simp] lemma toUltrastrongStar_neg (x : M) :
   toUltrastrongStar 𝕜 M P (-x) = -toUltrastrongStar 𝕜 M P x := rfl
 
-@[simp] lemma ofUltrastrongStar_neg (x : s*(M, P)_𝕜) :
+@[simp] lemma ofUltrastrongStar_neg (x : s⋆(M, P)_𝕜) :
   (-x).ofUltrastrongStar = -x.ofUltrastrongStar := rfl
 
 @[simp] lemma toUltrastrongStar_sub (x y : M) :
     toUltrastrongStar 𝕜 M P (x - y) = toUltrastrongStar 𝕜 M P x - toUltrastrongStar 𝕜 M P y := rfl
 
-@[simp] lemma ofUltrastrongStar_sub (x y : s*(M, P)_𝕜) :
+@[simp] lemma ofUltrastrongStar_sub (x y : s⋆(M, P)_𝕜) :
     (x - y).ofUltrastrongStar = x.ofUltrastrongStar - y.ofUltrastrongStar := rfl
 
 @[simp] lemma toUltrastrongStar_inj {x y : M} :
     toUltrastrongStar 𝕜 M P x = toUltrastrongStar 𝕜 M P y ↔ x = y :=
   equiv 𝕜 M P |>.symm.injective.eq_iff
 
-@[simp] lemma ofUltrastrongStar_inj {x y : s*(M, P)_𝕜} :
+@[simp] lemma ofUltrastrongStar_inj {x y : s⋆(M, P)_𝕜} :
     x.ofUltrastrongStar = y.ofUltrastrongStar ↔ x = y :=
   equiv 𝕜 M P |>.injective.eq_iff
 
 @[simp] lemma toUltrastrongStar_eq_zero {x : M} : toUltrastrongStar 𝕜 M P x = 0 ↔ x = 0 :=
   toUltrastrongStar_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ toUltrastrongStar_inj
 
-@[simp] lemma ofUltrastrongStar_eq_zero {x : s*(M, P)_𝕜} : x.ofUltrastrongStar = 0 ↔ x = 0 :=
+@[simp] lemma ofUltrastrongStar_eq_zero {x : s⋆(M, P)_𝕜} : x.ofUltrastrongStar = 0 ↔ x = 0 :=
   ofUltrastrongStar_zero (𝕜 := 𝕜) (M := M) (P := P) ▸ ofUltrastrongStar_inj
 
 /-! ## Equivalences -/
 
 variable (𝕜 M P) in
-/-- The canonical linear equivalence between `s*(M, P)_𝕜` and `M`. -/
+/-- The canonical linear equivalence between `s⋆(M, P)_𝕜` and `M`. -/
 @[expose, simps]
-def linearEquiv : s*(M, P)_𝕜 ≃ₗ[𝕜] M where
+def linearEquiv : s⋆(M, P)_𝕜 ≃ₗ[𝕜] M where
   toEquiv := equiv 𝕜 M P
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
@@ -112,7 +112,8 @@ open ComplexOrder PositiveLinearMap
 open Ultraweak in
 /-- Seminorm family for the ultrastrong-star topology. -/
 noncomputable def seminormFamily : SeminormFamily ℂ
-    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2) s*(M, P) :=
+    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2) s⋆
+  (M, P) :=
   fun f ↦ if f.2 = 0 then normSeminorm ℂ f.1.val.PreGNS' |>.comp
     (linearEquiv ℂ M P |>.trans f.1.val.toPreGNS').toLinearMap else
       normSeminorm ℂ f.1.val.PreGNS' |>.comp <|
@@ -120,12 +121,12 @@ noncomputable def seminormFamily : SeminormFamily ℂ
           (starLinearEquiv ℂ (A := M)) |>.toLinearMap
 
 /-- Filter basis for the seminorm family for the ultrastrong-star topology. -/
-noncomputable def filterBasis : ModuleFilterBasis ℂ s*(M, P) := seminormFamily.moduleFilterBasis
+noncomputable def filterBasis : ModuleFilterBasis ℂ s⋆(M, P) := seminormFamily.moduleFilterBasis
 
-noncomputable instance : TopologicalSpace s*(M, P) := filterBasis.topology'
+noncomputable instance : TopologicalSpace s⋆(M, P) := filterBasis.topology'
 
 /-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
-lemma withSeminorms : WithSeminorms (E := s*(M, P)) seminormFamily :=
+lemma withSeminorms : WithSeminorms (E := s⋆(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
 end UltrastrongStar

From 669fa771cad6b7952bb8d562a7e56d6504154d61 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 07:52:24 -0400
Subject: [PATCH 19/43] fixed small breakage

---
 LeanOA/UltrastrongStar.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 5f43feff..1b6b0486 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -112,8 +112,8 @@ open ComplexOrder PositiveLinearMap
 open Ultraweak in
 /-- Seminorm family for the ultrastrong-star topology. -/
 noncomputable def seminormFamily : SeminormFamily ℂ
-    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2) s⋆
-  (M, P) :=
+    (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2)
+    s⋆(M, P) :=
   fun f ↦ if f.2 = 0 then normSeminorm ℂ f.1.val.PreGNS' |>.comp
     (linearEquiv ℂ M P |>.trans f.1.val.toPreGNS').toLinearMap else
       normSeminorm ℂ f.1.val.PreGNS' |>.comp <|

From 42c7520d299dbaff4339bcc16e2767369a80a5ce Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 07:58:13 -0400
Subject: [PATCH 20/43] lake exe mk_all

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

diff --git a/LeanOA.lean b/LeanOA.lean
index 1a0a99a9..5e80544e 100644
--- a/LeanOA.lean
+++ b/LeanOA.lean
@@ -58,6 +58,7 @@ public import LeanOA.Predual
 public import LeanOA.TendstoZero.Defs
 public import LeanOA.TendstoZero.StrongDual
 public import LeanOA.Ultrastrong
+public import LeanOA.UltrastrongStar
 public import LeanOA.Ultraweak.Basic
 public import LeanOA.Ultraweak.Bornology
 public import LeanOA.Ultraweak.ContinuousFunctionalCalculus

From 0b23023c2971a36daff1f0b06ea2a4f54107cd63 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 5 Jun 2026 14:51:28 +0100
Subject: [PATCH 21/43] random cleanups

---
 LeanOA/Ultrastrong.lean     |  7 +++++--
 LeanOA/UltrastrongStar.lean | 11 ++++++-----
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index fc96e5fe..9e1e1ebc 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -89,12 +89,14 @@ instance : Module 𝕜 (s(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
 
 variable (𝕜 M P) in
 /-- The canonical linear equivalence between `s(M, P)_𝕜` and `M`. -/
-@[expose, simps]
+@[expose, simps!]
 def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
   toEquiv := equiv 𝕜 M P
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
+@[simp] lemma toEquiv_linearEquiv : (linearEquiv 𝕜 M P).toEquiv = equiv 𝕜 M P := rfl
+
 /-! ## The Topology -/
 
 variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
@@ -104,12 +106,13 @@ variable [StarModule ℂ M] [SelfAdjointDecompose M]
 open ComplexOrder PositiveLinearMap
 
 /-- Seminorm family for the ultrastrong topology. -/
-noncomputable def seminormFamily : SeminormFamily ℂ
+@[expose] noncomputable def seminormFamily : SeminormFamily ℂ
     (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))}) s(M, P) :=
   fun f ↦ (normSeminorm ℂ (f.val.PreGNS')).comp
     ((linearEquiv ℂ M P).trans f.val.toPreGNS').toLinearMap
 
 /-- Filter basis for the seminorm family for the ultrastrong topology. -/
+@[expose]
 noncomputable def filterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.moduleFilterBasis
 
 noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 1b6b0486..5ceee70c 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -15,17 +15,17 @@ def UltrastrongStar (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
 
 @[inherit_doc]
-scoped[UltrastrongStar] notation "s⋆("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
+scoped[Ultrastrong] notation "s⋆("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
 @[inherit_doc]
-scoped[UltrastrongStar] notation "s⋆("M", " P")" => UltrastrongStar ℂ M P
+scoped[Ultrastrong] notation "s⋆("M", " P")" => UltrastrongStar ℂ M P
+
+open scoped Ultrastrong
 
 /-! ## Linear structure -/
 
 variable {𝕜 M P : Type*} [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
   [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P]
 
-open UltrastrongStar
-
 variable (𝕜 M P) in
 /-- The canonical map from `M` to `s⋆(M, P)_𝕜`. -/
 @[expose] def toUltrastrongStar (x : M) : s⋆(M, P)_𝕜 := x
@@ -111,7 +111,7 @@ open ComplexOrder PositiveLinearMap
 
 open Ultraweak in
 /-- Seminorm family for the ultrastrong-star topology. -/
-noncomputable def seminormFamily : SeminormFamily ℂ
+@[expose] noncomputable def seminormFamily : SeminormFamily ℂ
     (ι := { f : M →ₚ[ℂ] ℂ // Continuous (f ∘ ofUltraweak (𝕜 := ℂ) (P := P))} × Fin 2)
     s⋆(M, P) :=
   fun f ↦ if f.2 = 0 then normSeminorm ℂ f.1.val.PreGNS' |>.comp
@@ -121,6 +121,7 @@ noncomputable def seminormFamily : SeminormFamily ℂ
           (starLinearEquiv ℂ (A := M)) |>.toLinearMap
 
 /-- Filter basis for the seminorm family for the ultrastrong-star topology. -/
+@[expose]
 noncomputable def filterBasis : ModuleFilterBasis ℂ s⋆(M, P) := seminormFamily.moduleFilterBasis
 
 noncomputable instance : TopologicalSpace s⋆(M, P) := filterBasis.topology'

From 789de2d317a09381595fde917c9ba4eba9b37134 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 10:52:26 -0400
Subject: [PATCH 22/43] Discrepency in comment/docstring

---
 LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
index df94d36e..b5de82ee 100644
--- a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
+++ b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
@@ -517,7 +517,7 @@ lemma continuous_seminorm_comp [TopologicalSpace E] [IsTopologicalAddGroup E]
 
 open LinearMap WithSeminorms
 
-/-- The continuous linear equivalence between `E` satisfiying `B.flip.IsCompatibleDual` and
+/-- The continuous linear equivalence between `E` satisfiying `B.IsCompatibleDual` and
 `PolarTopology B (nhdsPolars B)`. -/
 def polarTopologyNhdsPolars [TopologicalSpace E] [IsTopologicalAddGroup E]
     [ContinuousSMul 𝕜 E] [hLCS : LocallyConvexSpace 𝕜 E]

From b2552a146b967665795d186ac63748c5e3d7124e Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Fri, 5 Jun 2026 18:03:03 +0100
Subject: [PATCH 23/43] ultrastrong* is stronger than ultrastrong

---
 LeanOA/Ultrastrong.lean     |  4 ++--
 LeanOA/UltrastrongStar.lean | 14 +++++++++++---
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 9e1e1ebc..cb554287 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -9,7 +9,8 @@ public import Mathlib.Analysis.Normed.Module.TransferInstance
 public section
 
 set_option linter.unusedVariables false in
-/-- Type synonym for `M` with the ultrastrong topology. -/
+/-- Type synonym for `M` with the ultrastrong topology.
+Notation for this is `s(M, P)_𝕜` or `s(M, P)` when `𝕜 = ℂ` (this is scped to `Ultrastrong`). -/
 @[expose, nolint unusedArguments]
 def Ultrastrong (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
@@ -117,7 +118,6 @@ noncomputable def filterBasis : ModuleFilterBasis ℂ s(M, P) := seminormFamily.
 
 noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 
-/-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
 lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 5ceee70c..8cd5509a 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -1,6 +1,7 @@
 module
 
 public import LeanOA.Predual
+public import LeanOA.Ultrastrong
 public import LeanOA.Ultraweak.Basic
 public import LeanOA.CStarAlgebra.PositiveLinearFunctional
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
@@ -9,7 +10,8 @@ public import Mathlib.Analysis.Normed.Module.TransferInstance
 public section
 
 set_option linter.unusedVariables false in
-/-- Type synonym for `M` with the ultrastrong-star topology. -/
+/-- Type synonym for `M` with the ultrastrong-⋆ topology.
+Notation for this is `s⋆(M, P)_𝕜` or `s⋆(M, P)` when `𝕜 = ℂ` (this is scped to `Ultrastrong`). -/
 @[expose, nolint unusedArguments]
 def UltrastrongStar (𝕜 M P : Type*) [RCLike 𝕜] [NormedRing M] [StarRing M] [NormedAlgebra 𝕜 M]
     [NormedAddCommGroup P] [NormedSpace 𝕜 P] [Predual 𝕜 M P] := M
@@ -95,7 +97,7 @@ instance : Module 𝕜 (s⋆(M, P)_𝕜) := equiv 𝕜 M P |>.module 𝕜
 
 variable (𝕜 M P) in
 /-- The canonical linear equivalence between `s⋆(M, P)_𝕜` and `M`. -/
-@[expose, simps]
+@[expose, simps!]
 def linearEquiv : s⋆(M, P)_𝕜 ≃ₗ[𝕜] M where
   toEquiv := equiv 𝕜 M P
   map_add' _ _ := rfl
@@ -126,8 +128,14 @@ noncomputable def filterBasis : ModuleFilterBasis ℂ s⋆(M, P) := seminormFami
 
 noncomputable instance : TopologicalSpace s⋆(M, P) := filterBasis.topology'
 
-/-- This is probably a stupid definition, but in case we want `WithSeminorms`. -/
 lemma withSeminorms : WithSeminorms (E := s⋆(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
+/-- Ultrastrong-⋆ topology is stronger than the ultrastrong. -/
+lemma continuous_toUltrastrong_ofUltrastrongStar :
+    Continuous (fun x : s⋆(M, P) ↦ toUltrastrong ℂ M P x.ofUltrastrongStar) :=
+  withSeminorms.continuous_of_isBounded Ultrastrong.withSeminorms
+    ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
+    fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
+
 end UltrastrongStar

From ad04ed235c6b0e299c5b350e6d3617f002f9d7e9 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 21:43:04 -0400
Subject: [PATCH 24/43] Part of `IsCompatibleDual` instanvce for the
 `Ultraweak` bilinear form...but I need to finish and rearrange...

---
 LeanOA/UltrastrongStar.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 8cd5509a..b144eb26 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -6,6 +6,7 @@ public import LeanOA.Ultraweak.Basic
 public import LeanOA.CStarAlgebra.PositiveLinearFunctional
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import Mathlib.Analysis.Normed.Module.TransferInstance
+public import LeanOA.Mathlib.Analysis.LocallyConvex.Bipolar
 
 public section
 
@@ -138,4 +139,19 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
+open WeakBilin
+
+instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
+    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
+    (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
+      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual := by
+apply LinearEquiv.IsCompatibleDual <|
+  pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual |>.toLinearEquiv.toLinearMap))
+· sorry
+· apply LinearMap.rightDualEquiv _ <|
+   (LinearMap.separatingRight_congr_iff (B := topDualPairing 𝕜 Q)
+    (Predual.equivDual).toLinearEquiv.symm <| LinearEquiv.refl 𝕜 Q).mpr
+      topDualPairing_separatingRight
+
+
 end UltrastrongStar

From b7da19845c0d13cd2ccd78b913e25db95ba659d5 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 21:56:42 -0400
Subject: [PATCH 25/43] Finished the IsCompatibleDual instance for Ultraweak.
 Will relocate it next.

---
 LeanOA/UltrastrongStar.lean | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index b144eb26..b6a411a9 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -144,14 +144,12 @@ open WeakBilin
 instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
     [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
     (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
-      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual := by
-apply LinearEquiv.IsCompatibleDual <|
-  pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual |>.toLinearEquiv.toLinearMap))
-· sorry
-· apply LinearMap.rightDualEquiv _ <|
-   (LinearMap.separatingRight_congr_iff (B := topDualPairing 𝕜 Q)
-    (Predual.equivDual).toLinearEquiv.symm <| LinearEquiv.refl 𝕜 Q).mpr
-      topDualPairing_separatingRight
-
+      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual :=
+  LinearEquiv.IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ
+    (Predual.equivDual |>.toLinearEquiv.toLinearMap)))
+      (LinearMap.rightDualEquiv _ <|
+        (LinearMap.separatingRight_congr_iff (Predual.equivDual).toLinearEquiv.symm
+          <| LinearEquiv.refl 𝕜 Q).mpr topDualPairing_separatingRight)
+            <| LinearMap.ext_iff₂.mpr fun _ ↦ congrFun rfl
 
 end UltrastrongStar

From a7ebcf952a0f53bb594746375bbba13815fe50cd Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 21:56:44 -0400
Subject: [PATCH 26/43] Will locate next.

---
 LeanOA/UltrastrongStar.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index b6a411a9..8e445231 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -139,8 +139,7 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
-open WeakBilin
-
+open WeakBilin in
 instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
     [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
     (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)

From 60da9bb4be7445b574e203c4c8e9b5b95a2a655a Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 22:04:52 -0400
Subject: [PATCH 27/43] I think this is located in an ok spot for the moment.

---
 LeanOA/Ultraweak/Basic.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index efe9dc04..3858db01 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -5,6 +5,7 @@ public import Mathlib.Analysis.InnerProductSpace.Basic
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import LeanOA.Mathlib.Analysis.RCLike.Extend
 public import LeanOA.Predual
+public import LeanOA.Mathlib.Analysis.LocallyConvex.Bipolar
 
 @[expose] public section
 
@@ -439,4 +440,18 @@ lemma toLinearEquiv_algEquiv : (algEquiv M P).toLinearEquiv = linearEquiv .. :=
 
 end Unital
 
+open WeakBilin in
+/-- The following is the `IsCompatibleDual` instance for the type-appropriate bilinear form
+  associated to `Ultraweak 𝕜 E`. -/
+instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
+    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
+    (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
+      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual :=
+  LinearEquiv.IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ
+    (Predual.equivDual |>.toLinearEquiv.toLinearMap)))
+      (LinearMap.rightDualEquiv _ <|
+        (LinearMap.separatingRight_congr_iff (Predual.equivDual).toLinearEquiv.symm
+          <| LinearEquiv.refl ..).mpr topDualPairing_separatingRight)
+            <| LinearMap.ext_iff₂.mpr fun _ ↦ congrFun rfl
+
 end Ultraweak

From 3eb3a1b3c97fc569a0271a21d434e7c588335ea8 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 22:05:06 -0400
Subject: [PATCH 28/43] removed ultraweak thing

---
 LeanOA/UltrastrongStar.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 8e445231..95f1ef57 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -139,16 +139,4 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
-open WeakBilin in
-instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
-    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
-    (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
-      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual :=
-  LinearEquiv.IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ
-    (Predual.equivDual |>.toLinearEquiv.toLinearMap)))
-      (LinearMap.rightDualEquiv _ <|
-        (LinearMap.separatingRight_congr_iff (Predual.equivDual).toLinearEquiv.symm
-          <| LinearEquiv.refl 𝕜 Q).mpr topDualPairing_separatingRight)
-            <| LinearMap.ext_iff₂.mpr fun _ ↦ congrFun rfl
-
 end UltrastrongStar

From 3b1fefdea6067702a3854473f8e647d151f0ae60 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 22:28:26 -0400
Subject: [PATCH 29/43] A bit more brevity

---
 LeanOA/Ultraweak/Basic.lean | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index 3858db01..ca991513 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -440,18 +440,15 @@ lemma toLinearEquiv_algEquiv : (algEquiv M P).toLinearEquiv = linearEquiv .. :=
 
 end Unital
 
-open WeakBilin in
+open WeakBilin LinearEquiv LinearMap in
 /-- The following is the `IsCompatibleDual` instance for the type-appropriate bilinear form
   associated to `Ultraweak 𝕜 E`. -/
 instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
     [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
-    (pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
-      |>.toLinearEquiv.toLinearMap))).IsCompatibleDual :=
-  LinearEquiv.IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ
-    (Predual.equivDual |>.toLinearEquiv.toLinearMap)))
-      (LinearMap.rightDualEquiv _ <|
-        (LinearMap.separatingRight_congr_iff (Predual.equivDual).toLinearEquiv.symm
-          <| LinearEquiv.refl ..).mpr topDualPairing_separatingRight)
-            <| LinearMap.ext_iff₂.mpr fun _ ↦ congrFun rfl
+    pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
+      |>.toLinearEquiv.toLinearMap)) |>.IsCompatibleDual :=
+  IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ Predual.equivDual.toLinearEquiv.toLinearMap))
+      (rightDualEquiv _ <| (separatingRight_congr_iff Predual.equivDual.toLinearEquiv.symm
+          <| refl ..).mpr topDualPairing_separatingRight) <| ext_iff₂.mpr fun _ ↦ congrFun rfl
 
 end Ultraweak

From eabbe30afd1a5611b9242f17b462f02f335c8835 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 22:31:31 -0400
Subject: [PATCH 30/43] A little shorter

---
 LeanOA/Ultraweak/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index ca991513..aad8cab8 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -440,15 +440,15 @@ lemma toLinearEquiv_algEquiv : (algEquiv M P).toLinearEquiv = linearEquiv .. :=
 
 end Unital
 
-open WeakBilin LinearEquiv LinearMap in
+open WeakBilin LinearEquiv LinearMap Predual in
 /-- The following is the `IsCompatibleDual` instance for the type-appropriate bilinear form
   associated to `Ultraweak 𝕜 E`. -/
 instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
     [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
-    pairing (topDualPairing 𝕜 Q ∘ₗ (Predual.equivDual (M := E)
-      |>.toLinearEquiv.toLinearMap)) |>.IsCompatibleDual :=
-  IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ Predual.equivDual.toLinearEquiv.toLinearMap))
-      (rightDualEquiv _ <| (separatingRight_congr_iff Predual.equivDual.toLinearEquiv.symm
-          <| refl ..).mpr topDualPairing_separatingRight) <| ext_iff₂.mpr fun _ ↦ congrFun rfl
+    pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E) |>.toLinearEquiv.toLinearMap))
+      |>.IsCompatibleDual :=
+  IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ equivDual.toLinearEquiv.toLinearMap))
+      (rightDualEquiv _ <| (separatingRight_congr_iff equivDual.toLinearEquiv.symm <| refl ..).mpr
+        topDualPairing_separatingRight) <| ext_iff₂.mpr fun _ ↦ congrFun rfl
 
 end Ultraweak

From 82edc74b085bb68f223fe14d5e47a52c8cc9355c Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Fri, 5 Jun 2026 22:35:42 -0400
Subject: [PATCH 31/43] Ok. Last one...

---
 LeanOA/Ultraweak/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index aad8cab8..5ef712ad 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -445,7 +445,7 @@ open WeakBilin LinearEquiv LinearMap Predual in
   associated to `Ultraweak 𝕜 E`. -/
 instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
     [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
-    pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E) |>.toLinearEquiv.toLinearMap))
+    pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E)).toLinearEquiv.toLinearMap)
       |>.IsCompatibleDual :=
   IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ equivDual.toLinearEquiv.toLinearMap))
       (rightDualEquiv _ <| (separatingRight_congr_iff equivDual.toLinearEquiv.symm <| refl ..).mpr

From 818b12536e7217091d9c643402196126bce5abeb Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 6 Jun 2026 09:12:25 -0400
Subject: [PATCH 32/43] Added `Ultrastrong.bilin` and `UltrastrongStar.bilin`.
 I introduced these as variants of B.flip rather than B, since this was what
 we did for `PolarTopology.bilin`, but this leads to the `IsCompatibleDual`
 instances requiring an extra flip...so I'm not sure we shouldn't go back and
 change these all to be about B and not B.flip.

---
 LeanOA/Ultrastrong.lean     | 6 ++++++
 LeanOA/UltrastrongStar.lean | 6 ++++++
 2 files changed, 12 insertions(+)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index cb554287..89cbcf76 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -98,6 +98,12 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
 
 @[simp] lemma toEquiv_linearEquiv : (linearEquiv 𝕜 M P).toEquiv = equiv 𝕜 M P := rfl
 
+/-- Variant of `(TopDualPairing 𝕜 P).flip` with
+  the type synonym `s(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
+abbrev bilin : P →ₗ[𝕜] s(M, P)_𝕜 →ₗ[𝕜] 𝕜 :=
+  ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap)) |>.flip
+
 /-! ## The Topology -/
 
 variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 95f1ef57..bfa7bbfb 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -104,6 +104,12 @@ def linearEquiv : s⋆(M, P)_𝕜 ≃ₗ[𝕜] M where
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
+/-- Variant of `(TopDualPairing 𝕜 P).flip` with
+  the type synonym `s⋆(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
+abbrev bilin : P →ₗ[𝕜] s⋆(M, P)_𝕜 →ₗ[𝕜] 𝕜 :=
+  ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap)) |>.flip
+
 /-! ## The Topology -/
 
 variable {M P : Type*} [NormedRing M] [PartialOrder M] [StarRing M] [StarOrderedRing M]

From 190dd7dbe38170d18c1f9727d32e8909c81c651b Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 6 Jun 2026 09:21:40 -0400
Subject: [PATCH 33/43] Reverted changed docstring for the moment, awaiting
 discussion.

---
 LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
index b5de82ee..44339e27 100644
--- a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
+++ b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
@@ -517,7 +517,13 @@ lemma continuous_seminorm_comp [TopologicalSpace E] [IsTopologicalAddGroup E]
 
 open LinearMap WithSeminorms
 
-/-- The continuous linear equivalence between `E` satisfiying `B.IsCompatibleDual` and
+/- I've changed the following docstring back to what it was, as I previously replaced
+ `B.flip` by `B` since the statement of the def has `B.IsCompatibleDual` and not
+ `B.flip.IsCompatibleDual`, but I want to clarify why we originally had the docstring like
+ this. I mean, the math doesn't lie, but I'm concerned that there was a good reason before
+ for us to have this as `B.flip`. Will keep thinking about it, but wanted to flag it here. -/
+
+/-- The continuous linear equivalence between `E` satisfiying `B.flip.IsCompatibleDual` and
 `PolarTopology B (nhdsPolars B)`. -/
 def polarTopologyNhdsPolars [TopologicalSpace E] [IsTopologicalAddGroup E]
     [ContinuousSMul 𝕜 E] [hLCS : LocallyConvexSpace 𝕜 E]

From 178ac395fb3bfd08d12f5143a910d0c4f59da155 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 6 Jun 2026 09:26:25 -0400
Subject: [PATCH 34/43] Added suggestion as to why that .flip must have shown
 up in the docstring.

---
 LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
index 44339e27..4316e9eb 100644
--- a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
+++ b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
@@ -521,7 +521,9 @@ open LinearMap WithSeminorms
  `B.flip` by `B` since the statement of the def has `B.IsCompatibleDual` and not
  `B.flip.IsCompatibleDual`, but I want to clarify why we originally had the docstring like
  this. I mean, the math doesn't lie, but I'm concerned that there was a good reason before
- for us to have this as `B.flip`. Will keep thinking about it, but wanted to flag it here. -/
+ for us to have this as `B.flip`. Will keep thinking about it, but wanted to flag it here.
+ I wonder if it is perhaps because we made `bilin` above a version of `B.flip` rather than `B`.
+ No `bilin` occurs in the statement below, though... -/
 
 /-- The continuous linear equivalence between `E` satisfiying `B.flip.IsCompatibleDual` and
 `PolarTopology B (nhdsPolars B)`. -/

From f634f6ec3c1c4f0f322acbb8585a114ab0896cec Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 7 Jun 2026 14:50:26 -0400
Subject: [PATCH 35/43] Added `Ultraweak.pairing` and changed
 `Ultrastrong.bilin` and `UltrastrongStar.bilin` into `Ultrastrong.pairing`
 and `UltrastrongStar.pairing`...perhaps we have that `bilin` is the flip of
 `pairing` throughout these files? Maybe that needs more clarity?

---
 .../Topology/Algebra/Module/PolarTopology.lean | 10 +---------
 LeanOA/Ultrastrong.lean                        |  6 +++---
 LeanOA/UltrastrongStar.lean                    |  6 +++---
 LeanOA/Ultraweak/Basic.lean                    | 18 ++++++++++++------
 4 files changed, 19 insertions(+), 21 deletions(-)

diff --git a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
index 4316e9eb..b5de82ee 100644
--- a/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
+++ b/LeanOA/Mathlib/Topology/Algebra/Module/PolarTopology.lean
@@ -517,15 +517,7 @@ lemma continuous_seminorm_comp [TopologicalSpace E] [IsTopologicalAddGroup E]
 
 open LinearMap WithSeminorms
 
-/- I've changed the following docstring back to what it was, as I previously replaced
- `B.flip` by `B` since the statement of the def has `B.IsCompatibleDual` and not
- `B.flip.IsCompatibleDual`, but I want to clarify why we originally had the docstring like
- this. I mean, the math doesn't lie, but I'm concerned that there was a good reason before
- for us to have this as `B.flip`. Will keep thinking about it, but wanted to flag it here.
- I wonder if it is perhaps because we made `bilin` above a version of `B.flip` rather than `B`.
- No `bilin` occurs in the statement below, though... -/
-
-/-- The continuous linear equivalence between `E` satisfiying `B.flip.IsCompatibleDual` and
+/-- The continuous linear equivalence between `E` satisfiying `B.IsCompatibleDual` and
 `PolarTopology B (nhdsPolars B)`. -/
 def polarTopologyNhdsPolars [TopologicalSpace E] [IsTopologicalAddGroup E]
     [ContinuousSMul 𝕜 E] [hLCS : LocallyConvexSpace 𝕜 E]
diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 89cbcf76..e66e027b 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -98,11 +98,11 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
 
 @[simp] lemma toEquiv_linearEquiv : (linearEquiv 𝕜 M P).toEquiv = equiv 𝕜 M P := rfl
 
-/-- Variant of `(TopDualPairing 𝕜 P).flip` with
+/-- Variant of `TopDualPairing 𝕜 P` with
   the type synonym `s(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
-abbrev bilin : P →ₗ[𝕜] s(M, P)_𝕜 →ₗ[𝕜] 𝕜 :=
+abbrev pairing : s(M, P)_𝕜 →ₗ[𝕜] P →ₗ[𝕜] 𝕜 :=
   ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
-    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap)) |>.flip
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap))
 
 /-! ## The Topology -/
 
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index bfa7bbfb..90fd8a48 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -104,11 +104,11 @@ def linearEquiv : s⋆(M, P)_𝕜 ≃ₗ[𝕜] M where
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
-/-- Variant of `(TopDualPairing 𝕜 P).flip` with
+/-- Variant of `TopDualPairing 𝕜 P` with
   the type synonym `s⋆(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
-abbrev bilin : P →ₗ[𝕜] s⋆(M, P)_𝕜 →ₗ[𝕜] 𝕜 :=
+abbrev pairing : s⋆(M, P)_𝕜 →ₗ[𝕜] P →ₗ[𝕜] 𝕜 :=
   ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
-    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap)) |>.flip
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap))
 
 /-! ## The Topology -/
 
diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index 5ef712ad..9e667541 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -440,14 +440,20 @@ lemma toLinearEquiv_algEquiv : (algEquiv M P).toLinearEquiv = linearEquiv .. :=
 
 end Unital
 
-open WeakBilin LinearEquiv LinearMap Predual in
+variable (𝕜 E Q : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
+    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q]
+
+open LinearEquiv LinearMap Predual
+
+/-- Variant of `TopDualPairing 𝕜 P` with
+  the type synonym `σ(E, Q)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
+noncomputable abbrev pairing : σ(E, Q)_𝕜 →ₗ[𝕜] Q →ₗ[𝕜] 𝕜 :=
+  WeakBilin.pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E)).toLinearEquiv.toLinearMap)
+
 /-- The following is the `IsCompatibleDual` instance for the type-appropriate bilinear form
   associated to `Ultraweak 𝕜 E`. -/
-instance {𝕜 E Q : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
-    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q] :
-    pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E)).toLinearEquiv.toLinearMap)
-      |>.IsCompatibleDual :=
-  IsCompatibleDual (pairing (topDualPairing 𝕜 Q ∘ₗ equivDual.toLinearEquiv.toLinearMap))
+instance : pairing 𝕜 E Q |>.IsCompatibleDual :=
+  IsCompatibleDual (pairing 𝕜 E Q)
       (rightDualEquiv _ <| (separatingRight_congr_iff equivDual.toLinearEquiv.symm <| refl ..).mpr
         topDualPairing_separatingRight) <| ext_iff₂.mpr fun _ ↦ congrFun rfl
 

From e4e90395f12d490546f69387d93ccb2715ab0530 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 7 Jun 2026 14:54:00 -0400
Subject: [PATCH 36/43] Standardized notation in the Ultraweak file and fixed
 small typo.

---
 LeanOA/Ultraweak/Basic.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/LeanOA/Ultraweak/Basic.lean b/LeanOA/Ultraweak/Basic.lean
index 9e667541..7308137c 100644
--- a/LeanOA/Ultraweak/Basic.lean
+++ b/LeanOA/Ultraweak/Basic.lean
@@ -440,20 +440,20 @@ lemma toLinearEquiv_algEquiv : (algEquiv M P).toLinearEquiv = linearEquiv .. :=
 
 end Unital
 
-variable (𝕜 E Q : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup Q]
-    [NormedSpace 𝕜 E] [NormedSpace 𝕜 Q] [Predual 𝕜 E Q]
+variable (𝕜 M P : Type*) [RCLike 𝕜] [NormedAddCommGroup M] [NormedAddCommGroup P]
+    [NormedSpace 𝕜 M] [NormedSpace 𝕜 P] [Predual 𝕜 M P]
 
 open LinearEquiv LinearMap Predual
 
 /-- Variant of `TopDualPairing 𝕜 P` with
-  the type synonym `σ(E, Q)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
-noncomputable abbrev pairing : σ(E, Q)_𝕜 →ₗ[𝕜] Q →ₗ[𝕜] 𝕜 :=
-  WeakBilin.pairing (topDualPairing 𝕜 Q ∘ₗ (equivDual (M := E)).toLinearEquiv.toLinearMap)
+  the type synonym `σ(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
+noncomputable abbrev pairing : σ(M, P)_𝕜 →ₗ[𝕜] P →ₗ[𝕜] 𝕜 :=
+  WeakBilin.pairing (topDualPairing 𝕜 P ∘ₗ equivDual.toLinearEquiv.toLinearMap)
 
 /-- The following is the `IsCompatibleDual` instance for the type-appropriate bilinear form
-  associated to `Ultraweak 𝕜 E`. -/
-instance : pairing 𝕜 E Q |>.IsCompatibleDual :=
-  IsCompatibleDual (pairing 𝕜 E Q)
+  associated to `σ(M, P)_𝕜`. -/
+instance : pairing 𝕜 M P |>.IsCompatibleDual :=
+  IsCompatibleDual (pairing 𝕜 M P)
       (rightDualEquiv _ <| (separatingRight_congr_iff equivDual.toLinearEquiv.symm <| refl ..).mpr
         topDualPairing_separatingRight) <| ext_iff₂.mpr fun _ ↦ congrFun rfl
 

From 58b354f528271fdb52af265a931872459e3cd342 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 7 Jun 2026 15:02:37 -0400
Subject: [PATCH 37/43] Don't know what changed here, but...

---
 LeanOA/Ultrastrong.lean     | 2 +-
 LeanOA/UltrastrongStar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index e66e027b..8c1dc32e 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -102,7 +102,7 @@ def linearEquiv : s(M, P)_𝕜 ≃ₗ[𝕜] M where
   the type synonym `s(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
 abbrev pairing : s(M, P)_𝕜 →ₗ[𝕜] P →ₗ[𝕜] 𝕜 :=
   ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
-    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap))
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual |>.toLinearEquiv.toLinearMap))
 
 /-! ## The Topology -/
 
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 90fd8a48..d3296f12 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -108,7 +108,7 @@ def linearEquiv : s⋆(M, P)_𝕜 ≃ₗ[𝕜] M where
   the type synonym `s⋆(M, P)_𝕜` in place of `P →L[𝕜] 𝕜`. -/
 abbrev pairing : s⋆(M, P)_𝕜 →ₗ[𝕜] P →ₗ[𝕜] 𝕜 :=
   ((linearEquiv 𝕜 M P).symm.arrowCongr (.refl _ _))
-    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual (M := M) |>.toLinearEquiv.toLinearMap))
+    (topDualPairing 𝕜 P ∘ₗ (Predual.equivDual |>.toLinearEquiv.toLinearMap))
 
 /-! ## The Topology -/
 

From 5d09ec748aee85365a29485abcf0b584823b7540 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 17 Jun 2026 08:31:33 -0400
Subject: [PATCH 38/43] included the natural uniformities. I'm not sure if this
 is the right transparency level (or the correct def, for that matter, since
 Jireh was uneasy about the uniformities.)

---
 LeanOA/Ultrastrong.lean     | 4 ++++
 LeanOA/UltrastrongStar.lean | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 8c1dc32e..9eb0e286 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -127,4 +127,8 @@ noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
+@[expose, implicit_reducible]
+noncomputable def uniformity : UniformSpace s(M, P) :=
+    IsTopologicalAddGroup.rightUniformSpace s(M, P)
+
 end Ultrastrong
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index d3296f12..29bbb327 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -145,4 +145,8 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
+@[expose, implicit_reducible]
+noncomputable def uniformity : UniformSpace s⋆(M, P) :=
+    IsTopologicalAddGroup.rightUniformSpace s⋆(M, P)
+
 end UltrastrongStar

From 848e7963a528fdf7cbb3162ab3470cf9c8c9eee6 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 17 Jun 2026 08:37:00 -0400
Subject: [PATCH 39/43] I think that if these are safe at all, they are
 probably safe as instances...

---
 LeanOA/Ultrastrong.lean     | 4 ++--
 LeanOA/UltrastrongStar.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 9eb0e286..ddf23f21 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -127,8 +127,8 @@ noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
-@[expose, implicit_reducible]
-noncomputable def uniformity : UniformSpace s(M, P) :=
+@[expose]
+noncomputable instance uniformity : UniformSpace s(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s(M, P)
 
 end Ultrastrong
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 29bbb327..af37b1d7 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -145,8 +145,8 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
-@[expose, implicit_reducible]
-noncomputable def uniformity : UniformSpace s⋆(M, P) :=
+@[expose]
+noncomputable instance uniformity : UniformSpace s⋆(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s⋆(M, P)
 
 end UltrastrongStar

From 9493a064ba4d88ac49e840168ddd12b33d024b3c Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 17 Jun 2026 08:55:35 -0400
Subject: [PATCH 40/43] Oops. Should let Lean name these.

---
 LeanOA/Ultrastrong.lean     | 2 +-
 LeanOA/UltrastrongStar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index ddf23f21..b9adfefb 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -128,7 +128,7 @@ lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
 @[expose]
-noncomputable instance uniformity : UniformSpace s(M, P) :=
+noncomputable instance : UniformSpace s(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s(M, P)
 
 end Ultrastrong
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index af37b1d7..d468dafa 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -146,7 +146,7 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
 @[expose]
-noncomputable instance uniformity : UniformSpace s⋆(M, P) :=
+noncomputable instance : UniformSpace s⋆(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s⋆(M, P)
 
 end UltrastrongStar

From d42cda4f7deaa7cc877cd24dfbf8dd04d66884a1 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 17 Jun 2026 10:57:10 -0400
Subject: [PATCH 41/43] Removed the `expose` tag from the new UniformSpace
 instances.

---
 LeanOA/Ultrastrong.lean     | 1 -
 LeanOA/UltrastrongStar.lean | 1 -
 2 files changed, 2 deletions(-)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index b9adfefb..6a888de6 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -127,7 +127,6 @@ noncomputable instance : TopologicalSpace s(M, P) := filterBasis.topology'
 lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
   { topology_eq_withSeminorms := rfl }
 
-@[expose]
 noncomputable instance : UniformSpace s(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s(M, P)
 
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index d468dafa..1054a7b0 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -145,7 +145,6 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
     ((Ultrastrong.linearEquiv ℂ M P).symm.toLinearMap ∘ₗ linearEquiv ℂ M P)
     fun i ↦ ⟨{(i, 0)}, 1, fun _ ↦ by simp [Ultrastrong.seminormFamily, seminormFamily]⟩
 
-@[expose]
 noncomputable instance : UniformSpace s⋆(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s⋆(M, P)
 

From 67db0dd7dcba3ed10d4ad78dc494a37ac6153548 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 17 Jun 2026 11:56:46 -0400
Subject: [PATCH 42/43] Added a comment on how to express the uniformity as an
 infimum of those from the individual seminorms, and added the needed
 IsUniformAddGroup instances needed to support this.

---
 LeanOA/Ultrastrong.lean     | 11 +++++++++++
 LeanOA/UltrastrongStar.lean | 11 +++++++++++
 2 files changed, 22 insertions(+)

diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index 6a888de6..ccac8e57 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -130,4 +130,15 @@ lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
 noncomputable instance : UniformSpace s(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s(M, P)
 
+noncomputable instance : IsUniformAddGroup s(M, P) :=
+  isUniformAddGroup_of_addCommGroup
+
+/-
+We have that the uniform structure induced by a family of seminorms is exactly the
+infimum of the ones induced by each seminorm individually. This
+is accessible as:
+`(SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf <|
+  seminormFamily (M := M) (P := P)).mp withSeminorms`
+-/
+
 end Ultrastrong
diff --git a/LeanOA/UltrastrongStar.lean b/LeanOA/UltrastrongStar.lean
index 1054a7b0..d1580ad6 100644
--- a/LeanOA/UltrastrongStar.lean
+++ b/LeanOA/UltrastrongStar.lean
@@ -148,4 +148,15 @@ lemma continuous_toUltrastrong_ofUltrastrongStar :
 noncomputable instance : UniformSpace s⋆(M, P) :=
     IsTopologicalAddGroup.rightUniformSpace s⋆(M, P)
 
+noncomputable instance : IsUniformAddGroup s⋆(M, P) :=
+  isUniformAddGroup_of_addCommGroup
+
+/-
+We have that the uniform structure induced by a family of seminorms is exactly the
+infimum of the ones induced by each seminorm individually. This
+is accessible as:
+`(SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf <|
+  seminormFamily (M := M) (P := P)).mp withSeminorms`
+-/
+
 end UltrastrongStar

From 43a20fb7eaeafcc9579a935921c445a66b95ec55 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 8 Jul 2026 12:15:15 -0400
Subject: [PATCH 43/43] Stub with comment. This was uncommitted from a while
 ago, so I'm not so sure it's the right way to go...got to get back on the
 horse, here.

---
 LeanOA/CStarAlgebra/Extreme.lean |  1 -
 LeanOA/Ultrastrong.lean          | 20 ++++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/LeanOA/CStarAlgebra/Extreme.lean b/LeanOA/CStarAlgebra/Extreme.lean
index ccd9e39b..df9292b5 100644
--- a/LeanOA/CStarAlgebra/Extreme.lean
+++ b/LeanOA/CStarAlgebra/Extreme.lean
@@ -248,7 +248,6 @@ theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (c
 
 attribute [local instance] IsUnital.toCStarAlgebra in
 /-- A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.
-
 To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/
 theorem CStarAlgebra.isUnital_iff :
     IsUnital A ↔ (extremePoints ℝ (closedBall (0 : A) 1)).Nonempty := by
diff --git a/LeanOA/Ultrastrong.lean b/LeanOA/Ultrastrong.lean
index ccac8e57..96c891e8 100644
--- a/LeanOA/Ultrastrong.lean
+++ b/LeanOA/Ultrastrong.lean
@@ -141,4 +141,24 @@ is accessible as:
   seminormFamily (M := M) (P := P)).mp withSeminorms`
 -/
 
+/-- The following is a primitive attempt to prove that the ultrastrong topology is
+stronger than the ultraweak. Note that there is a hold up here, in that there seems
+to be a need for a Jordan decomposition for the predual that we don't yet have access to.
+Maybe it's a good idea to see if we can prove that directly, and to then use it here to
+give a short proof of this continuity. In Sakai, however, the problem is approached
+differently, using extreme points etc. We keep this here as a stub in case the other
+approach faces difficulties and proves to be equally hard. -/
+theorem bar : Continuous ((toUltraweak ℂ P).comp (ofUltrastrong (𝕜 := ℂ) (M := M) (P:= P))) := by
+  apply WithSeminorms.continuous_of_isBounded
+     (Ultrastrong.withSeminorms)
+      (LinearMap.weakBilin_withSeminorms (Ultraweak.pairing ℂ M P))
+        ((Ultraweak.linearEquiv ℂ M P).toLinearMap.comp
+          (Ultrastrong.linearEquiv (𝕜 := ℂ) (M := M) (P:= P)).toLinearMap)
+  intro φ
+  sorry -- Now all we need is to prove IsBounded, however note the issue with postive
+  --functionals here.
+
+/- To induce the natural Star on dual objects, we should use starLinearEquiv. This makes
+me wonder if we should have a starContinuousLinearEquiv for ContinuousStar. -/
+
 end Ultrastrong