feat: Ultrastrong topology

LeanOA.lean

@@ -46,8 +46,11 @@ public import LeanOA.Mathlib.Topology.Algebra.UniformConvergence
 public import LeanOA.Mathlib.Topology.ContinuousMap.ContinuousMapZero
 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.UltrastrongStar
 public import LeanOA.Ultraweak.Basic
 public import LeanOA.Ultraweak.Bornology
 public import LeanOA.Ultraweak.ContinuousFunctionalCalculus

LeanOA/CStarAlgebra/Extreme.lean

@@ -249,7 +249,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

LeanOA/CStarAlgebra/PositiveLinearFunctional.lean

@@ -61,6 +61,7 @@ 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
 

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]

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

LeanOA/Ultrastrong.lean

@@ -0,0 +1,164 @@
+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 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
+
+@[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 `s(M, P)_𝕜`. -/
+@[expose] def toUltrastrong (x : M) : s(M, P)_𝕜 := 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 : 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 `s(M, P)_𝕜` and `M`. -/
+@[expose, simps] def equiv : s(M, P)_𝕜 ≃ M where
+  toFun := ofUltrastrong
+  invFun := toUltrastrong 𝕜 M P
+
+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 : 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 : 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 : 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_sub (x y : M) :
+    toUltrastrong 𝕜 M P (x - y) = toUltrastrong 𝕜 M P x - toUltrastrong 𝕜 M P y := rfl
+
+@[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 : 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 : 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
+  toEquiv := equiv 𝕜 M P
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+@[simp] lemma toEquiv_linearEquiv : (linearEquiv 𝕜 M P).toEquiv = equiv 𝕜 M P := rfl
+
+/-- Variant of `TopDualPairing 𝕜 P` with
+  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 |>.toLinearEquiv.toLinearMap))
+
+/-! ## 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
+
+/-- Seminorm family for the ultrastrong topology. -/
+@[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'
+
+lemma withSeminorms : WithSeminorms (E := s(M, P)) seminormFamily :=
+  { topology_eq_withSeminorms := rfl }
+
+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`
+-/
+
+/-- 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

LeanOA/UltrastrongStar.lean

@@ -0,0 +1,162 @@
+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
+public import Mathlib.Analysis.Normed.Module.TransferInstance
+public import LeanOA.Mathlib.Analysis.LocallyConvex.Bipolar
+
+public section
+
+set_option linter.unusedVariables false in
+/-- 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
+
+@[inherit_doc]
+scoped[Ultrastrong] notation "s⋆("M", " P")_" 𝕜:max => UltrastrongStar 𝕜 M P
+@[inherit_doc]
+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]
+
+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
+
+/-- Variant of `TopDualPairing 𝕜 P` with
+  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 |>.toLinearEquiv.toLinearMap))
+
+/-! ## 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
+
+open Ultraweak in
+/-- Seminorm family for the ultrastrong-star topology. -/
+@[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
+    (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. -/
+@[expose]
+noncomputable def filterBasis : ModuleFilterBasis ℂ s⋆(M, P) := seminormFamily.moduleFilterBasis
+
+noncomputable instance : TopologicalSpace s⋆(M, P) := filterBasis.topology'
+
+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]⟩
+
+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