TracialL2Closure.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The bounded elements in the L² closure of a star subalgebra form an actual norm-closed star subalgebra. Multiplication is obtained from the commuting left and right tracial actions, rather than assumed as a property of a proposed generated algebra.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.vector_continuous line 24
Source documentation
The algebra-vector map is norm continuous because it is the left representation evaluated at the identity vector.
```
theorem vector_continuous : Continuous G.vector := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_mono line 32
Source documentation
Inclusion of algebras induces inclusion of their closed Hilbert spans.
```
theorem baseSpace_mono {S T : StarSubalgebra ℂ P} (hST : S ≤ T) :
    G.baseSpace S ≤ G.baseSpace T := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_topologicalClosure line 41
Source documentation
Taking the norm closure of the algebra does not change its L² span.
```
theorem baseSpace_topologicalClosure (S : StarSubalgebra ℂ P) :
    G.baseSpace S.topologicalClosure = G.baseSpace S := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.left_preserves_baseSpace_of_vector_mem line 62
Source documentation
An element whose vector lies in the closed subspace preserves that subspace under left multiplication, by right multiplication on dense algebra vectors.
```
theorem left_preserves_baseSpace_of_vector_mem {x : P}
    (hx : G.vector x ∈ G.baseSpace S) (y : H) (hy : y ∈ G.baseSpace S) :
    G.left x y ∈ G.baseSpace S := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.conjugation_preserves_baseSpace line 76
Source documentation
The same closed subspace is preserved by tracial conjugation.
```
theorem conjugation_preserves_baseSpace (y : H) (hy : y ∈ G.baseSpace S) :
    G.conjugation y ∈ G.baseSpace S := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.l2ClosureAlgebra line 82
Source documentation
The actual bounded algebra lying in the L² closure of S.
```
def l2ClosureAlgebra : StarSubalgebra ℂ P where
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.mem_l2ClosureAlgebra line 107
instance OAI.KadisonSimilarity.TracialCornerGeometry.l2ClosureAlgebra_isClosed line 110
theorem OAI.KadisonSimilarity.TracialCornerGeometry.le_l2ClosureAlgebra line 115
Source documentation
Every original algebra element lies in the constructed bounded closure.
```
theorem le_l2ClosureAlgebra : S ≤ G.l2ClosureAlgebra S := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2ClosureAlgebra_vector_mem line 122
Source documentation
Membership gives exactly the required L² approximation by the original algebra vectors, with no additional generated-algebra hypothesis.
```
theorem l2ClosureAlgebra_vector_mem (x : G.l2ClosureAlgebra S) :
    G.vector (x : P) ∈ closure (Set.range (G.baseAlgebraVectors S)) := x.property
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_l2ClosureAlgebra line 127
Source documentation
Passing to the constructed bounded algebra leaves the Hilbert space unchanged.
```
theorem baseSpace_l2ClosureAlgebra : G.baseSpace (G.l2ClosureAlgebra S) = G.baseSpace S := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra line 140
Source documentation
The bounded L²-generated algebra of an arbitrary star subalgebra, constructed by first taking its norm closure.
```
def l2GeneratedAlgebra (S : StarSubalgebra ℂ P) : StarSubalgebra ℂ P := by
…
```
instance OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra_isClosed line 144
theorem OAI.KadisonSimilarity.TracialCornerGeometry.le_l2GeneratedAlgebra line 151
Source documentation
The original seed algebra is contained in its constructed L²-generated algebra.
```
theorem le_l2GeneratedAlgebra (S : StarSubalgebra ℂ P) : S ≤ G.l2GeneratedAlgebra S := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSpace_l2GeneratedAlgebra line 156
Source documentation
The generated algebra has precisely the original seed's Hilbert span.
```
theorem baseSpace_l2GeneratedAlgebra (S : StarSubalgebra ℂ P) :
    G.baseSpace (G.l2GeneratedAlgebra S) = G.baseSpace S := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra_vector_mem line 164
Source documentation
Algebra-vector density of the seed is built into the construction, including when the seed is merely the algebraic factor algebra.
```
theorem l2GeneratedAlgebra_vector_mem (S : StarSubalgebra ℂ P)
    (x : G.l2GeneratedAlgebra S) :
    G.vector (x : P) ∈ closure (Set.range (G.baseAlgebraVectors S)) := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra line 173
Source documentation
The concrete bounded algebra generated in L² by two prescribed factors.
```
def l2FactorAlgebra (A D : StarSubalgebra ℂ P) : StarSubalgebra ℂ P :=
…
```
instance OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra_isClosed line 176
theorem OAI.KadisonSimilarity.TracialCornerGeometry.left_le_l2FactorAlgebra line 180
theorem OAI.KadisonSimilarity.TracialCornerGeometry.right_le_l2FactorAlgebra line 185
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra_vector_mem line 192
Source documentation
Algebra vectors of the two generating factors are dense in the constructed algebra's tracial Hilbert space.
```
theorem l2FactorAlgebra_vector_mem (A D : StarSubalgebra ℂ P)
    (x : G.l2FactorAlgebra A D) :
    G.vector (x : P) ∈ closure (Set.range
      (G.vector.comp (factorAlgebra A D).subtype.toLinearMap)) :=
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.factorAlgebra
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra_generation line 200
Source documentation
In its concrete Hilbert subspace, the constructed algebra is generated by the two original factors.
```
theorem l2FactorAlgebra_generation (A D : StarSubalgebra ℂ P) :
    (G.baseGeometry (G.l2FactorAlgebra A D)).FactorsTraciallyGenerate
      (A.comap (G.l2FactorAlgebra A D).subtype)
      (D.comap (G.l2FactorAlgebra A D).subtype) :=
…
```
Mentions: OAI.KadisonSimilarity.TracialCornerGeometry.FactorsTraciallyGenerate
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra_native_generation line 212
Source documentation
The same generation statement holds in the canonical GNS model of the constructed algebra, without a separate density hypothesis.
```
theorem l2FactorAlgebra_native_generation (τ : P →ₚ[ℂ] ℂ)
    (htr : ∀ a b : P, τ (a * b) = τ (b * a)) (A D : StarSubalgebra ℂ P) :
    let L := (gnsTracialGeometry τ htr).l2FactorAlgebra A D
…
```
Mentions: OAI.KadisonSimilarity.gnsTracialGeometry, OAI.KadisonSimilarity.TracialCornerGeometry.l2FactorAlgebra