GeneratedDihedralAlgebras.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The two auxiliary algebras in the spectral test are the actual bounded L² closures of their algebraic generators. Their inclusions and the density premises in the free-corner theorem follow from this construction.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra_mono line 19
Source documentation
Bounded L² generation is monotone in its algebraic generators.
```
theorem l2GeneratedAlgebra_mono {S T : StarSubalgebra ℂ P} (hST : S ≤ T) :
    G.l2GeneratedAlgebra S ≤ G.l2GeneratedAlgebra T := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.l2GeneratedAlgebra_vector_mem_span line 31
Source documentation
The constructed algebra has precisely the algebra-vector density used in the Fourier test, in the linear-span formulation of that theorem.
```
theorem l2GeneratedAlgebra_vector_mem_span (S : StarSubalgebra ℂ P)
    (x : G.l2GeneratedAlgebra S) :
    G.vector (x : P) ∈ (Submodule.span ℂ
      (G.vector '' (S : Set P))).topologicalClosure := by
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.generatedDihedralAlgebra line 42
Source documentation
The finite dihedral von Neumann algebra, expressed through its bounded L² closure; no normal-form density is imposed as an extra premise.
```
def generatedDihedralAlgebra (d s : P) : StarSubalgebra ℂ P :=
…
```
def OAI.KadisonSimilarity.TracialCornerGeometry.generatedTestAlgebra line 47
Source documentation
The auxiliary algebra generated by the second factor and the test symmetry.
```
def generatedTestAlgebra (D : StarSubalgebra ℂ P) (s : P) : StarSubalgebra ℂ P :=
…
```
instance OAI.KadisonSimilarity.TracialCornerGeometry.generatedDihedralAlgebra_isClosed line 50
instance OAI.KadisonSimilarity.TracialCornerGeometry.generatedTestAlgebra_isClosed line 54
theorem OAI.KadisonSimilarity.TracialCornerGeometry.first_mem_generatedDihedralAlgebra line 58
theorem OAI.KadisonSimilarity.TracialCornerGeometry.second_mem_generatedDihedralAlgebra line 62
theorem OAI.KadisonSimilarity.TracialCornerGeometry.le_generatedTestAlgebra line 66
theorem OAI.KadisonSimilarity.TracialCornerGeometry.generatedDihedralAlgebra_le_test line 71
theorem OAI.KadisonSimilarity.TracialCornerGeometry.generatedDihedralAlgebra_density line 81
theorem OAI.KadisonSimilarity.TracialCornerGeometry.generatedTestAlgebra_density line 87