PointedPowerCyclicity.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Cyclic and separating configuration vacua

Local cyclicity generates every finitely excited basis vector. Applying the same argument to the commuting right actions proves separation.

def OAI.KadisonKastler.pointedPowerInsertLinear line 21
theorem OAI.KadisonKastler.pointedPowerInsertLinear_single line 27
theorem OAI.KadisonKastler.pointedPowerInsertLinear_operator line 33
def OAI.KadisonKastler.pointedPowerSite line 41
def OAI.KadisonKastler.pointedPowerAlgebra line 46
theorem OAI.KadisonKastler.pointedPowerSite_mem line 51
theorem OAI.KadisonKastler.pointedPowerBasis_mem_orbit line 58
theorem OAI.KadisonKastler.pointedPowerAlgebra_cyclic line 97
Source documentation
A local cyclic vector gives a cyclic vector for the countable product.
```
theorem pointedPowerAlgebra_cyclic
    (E : MatrixUnitSystem (Fin 2) (PointedLocalHilbert →L[ℂ] PointedLocalHilbert))
    (hE : Submodule.span ℂ (Set.range (fun p : Fin 2 × Fin 2 =>
      E.entry p.1 p.2 pointedLocalVacuum)) = ⊤) :
    DenseRange (algebraVectorMap (pointedPowerAlgebra E) pointedPowerVacuum) := by
…
```
Mentions: OAI.KadisonKastler.PointedLocalHilbert, OAI.KadisonKastler.pointedLocalVacuum, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.pointedPowerAlgebra, OAI.KadisonKastler.pointedPowerVacuum
theorem OAI.KadisonKastler.pointedPowerAlgebra_commutant line 117
theorem OAI.KadisonKastler.pointedPowerAlgebra_separating line 164
Source documentation
The commuting right cyclic vacuum separates the left product algebra.
```
theorem pointedPowerAlgebra_separating {ν : ℝ} (d : PointedLocalMatrixData ν) :
    Function.Injective (algebraVectorMap (pointedPowerAlgebra d.left) pointedPowerVacuum) := by
…
```
Mentions: OAI.KadisonKastler.PointedLocalMatrixData, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.pointedPowerAlgebra, OAI.KadisonKastler.pointedPowerVacuum