ExpectedModularRows.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The expected-state construction supplies all common right-action data. Only separate finite-row approximants are used in the graph comparison.

theorem OAI.KadisonKastler.exists_expected_modular_row_graph_comparison line 32
Source documentation
An expectation onto the finite common algebra supplies the right data; no global choice of a nearby operator is required.
```
theorem exists_expected_modular_row_graph_comparison
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding
theorem OAI.KadisonKastler.exists_expected_matrixStage_row_graph_comparison line 73
Source documentation
Actual increasing matrix stages supply injectivity. The expectation and modular conjugation supply the central vector and common right action.
```
theorem exists_expected_matrixStage_row_graph_comparison
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding