IncreasingMatrixPreparation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Increasing full matrix stages in the preparation argument

The finite-stage construction and the graph comparison use two equivalent presentations of the same concrete matrix algebras. Their generated von Neumann algebras agree, so approximate finite dimensionality gives injectivity on both sides of the prepared graph.

def OAI.KadisonKastler.matrixStageConcreteUnits line 24

Source documentation

The ambient matrix units of a finite stage.

def matrixStageConcreteUnits (A : ℕ → FiniteMatrixStage M) (n : ℕ) :
    MatrixUnitSystem (Fin (A n).size) (H →L[ℂ] H) :=
…

theorem OAI.KadisonKastler.matrixStageConcreteUnits_algebra line 28

theorem OAI.KadisonKastler.generated_matrixStages_eq line 39

Source documentation

The two actual closure constructions agree.

theorem generated_matrixStages_eq (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    FiniteMatrixStage.generatedVonNeumann A =
      generatedVonNeumannAlgebra (⨆ n, (matrixStageConcreteUnits A n).algebra) := by
…

Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.matrixStageConcreteUnits

theorem OAI.KadisonKastler.isInjective_generated_matrixStages line 57
Source documentation
The published increasing-matrix input applies directly to the matrix stages that enter the graph argument.
```
theorem isInjective_generated_matrixStages
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity
theorem OAI.KadisonKastler.exists_prepared_matrixStage_graph_comparison line 76
Source documentation
Actual increasing finite matrix stages supply both injectivity inputs in the generic preparation-to-graph theorem.
```
theorem exists_prepared_matrixStage_graph_comparison
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity