PreparedGraphRows.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Prepared graph comparison from individual row approximants

Only a separate nearby row is required for each finite row in either algebra. No global linear map selecting those approximants is assumed.

abbrev OAI.KadisonKastler.GraphRowApproximation line 27
Source documentation
The individual finite-row approximation property used in the graph construction. This notation imposes no compatibility among the choices.
```
abbrev GraphRowApproximation (M N : VonNeumannAlgebra H) (γ : ℝ) : Prop :=
…
```

theorem OAI.KadisonKastler.norm_prepared_rescaledGraphProjection_sub_le_of_row_approx line 34

Source documentation

Common matrix actions and two-sided individual row approximation imply the uniform comparison of every positively rescaled closed graph.

theorem norm_prepared_rescaledGraphProjection_sub_le_of_row_approx
    (M N : VonNeumannAlgebra H) (Ω : H) (hΩ : ‖Ω‖ = 1)
    (d : ℕ → ℕ) (E : ∀ n, Generator.MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hEM : ∀ n, (E n).algebra ≤ M.toStarSubalgebra)
    (hEN : ∀ n, (E n).algebra ≤ N.toStarSubalgebra)
    (hirrM : ∀ A ∈ M, (∀ n a, a ∈ (E n).algebra → a * A = A * a) →
      ∃ z : ℂ, A = z • (1 : H →L[ℂ] H))
    (hirrN : ∀ A ∈ N, (∀ n a, a ∈ (E n).algebra → a * A = A * a) →
      ∃ z : ℂ, A = z • (1 : H →L[ℂ] H))
    (hcentralM : ∀ n a, a ∈ (E n).algebra → ∀ z ∈ M,
      inner ℂ Ω ((a * z) Ω) = inner ℂ Ω ((z * a) Ω))
…

Mentions: OAI.Generator.MatrixUnitSystem