PointedPowerProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete Powers product and the pointed-product input

The countable configuration Hilbert space carries the faithful product of the two-dimensional diagonal state. Its commuting right action gives a separating vacuum; finite configuration vectors give cyclicity.

def OAI.KadisonKastler.constantPointedMatrixProduct line 23
Source documentation
A constant two-dimensional product with its actual matrix-state moments.
```
def constantPointedMatrixProduct {ν : ℝ} (hν : 0 < ν) (hν1 : ν < 1) :
    PointedMatrixProduct.{0} (fun _ : ℕ => ν) := by
…
```
def OAI.KadisonKastler.fixedPowersProduct line 41
Source documentation
The fixed lambda product required by the absorption argument.
```
def fixedPowersProduct : PointedMatrixProduct.{u} (fun _ : ℕ => fixedProductLambda) :=
…
```
Mentions: OAI.KadisonKastler.fixedProductLambda
theorem OAI.KadisonKastler.publishedPointedMatrixOperations line 45
Source documentation
Blackadar III.3.1.1--2, specialized to the exact operations used here.
```
theorem publishedPointedMatrixOperations : PublishedPointedMatrixOperations.{u} :=
…
```