PreparedRightGraphRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prepared right actions with individual row approximants

The finite matrix and common right-action arguments do not require a linear choice of nearby operators. These variants retain only the actual finite-row approximations supplied by matrix unit-ball proximity.

theorem OAI.KadisonKastler.norm_preparedRight_graphProjection_sub_le_of_row_approx line 30

Source documentation

Common right-action identities give all graph comparison hypotheses; individual row approximants suffice for the remaining analytic step.

theorem norm_preparedRight_graphProjection_sub_le_of_row_approx
    (M N R : VonNeumannAlgebra H)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hR : R = generatedVonNeumannAlgebra (⨆ n, (E n).algebra))
    (hRM : R ≤ M) (hRN : R ≤ N)
    (hirr : ∀ A ∈ M, (∀ a ∈ R, a * A = A * a) →
      ∃ z : ℂ, A = z • (1 : H →L[ℂ] H))
    (hgap : kkDistance M N < 1 / 2)
    (hrightM : ∀ r ∈ R, conjugationOperator J r ∈ M.commutant)
    (hrightN : ∀ r ∈ R, conjugationOperator J r ∈ N.commutant)
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.exists_preparedRight_row_graph_comparison line 94
Source documentation
The localized right correction is independent of the row approximants. After choosing it, every pair of row bounds gives the graph estimate.
```
theorem exists_preparedRight_row_graph_comparison
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding
theorem OAI.KadisonKastler.exists_prepared_matrixStage_row_graph_comparison line 135
Source documentation
The increasing-matrix injectivity input supplies both injectivity requirements in the row version of preparation.
```
theorem exists_prepared_matrixStage_row_graph_comparison
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity