PreparedGraphComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform graph comparison in a prepared pair

The genuine matrix averages and the two completely close linear maps supply every hypothesis of the row construction. The final estimate is uniform over all positive rescalings of the two closed Tomita graphs.

theorem OAI.KadisonKastler.norm_prepared_rescaledGraphProjection_sub_le line 28

Source documentation

Actual common matrix actions and complete map bounds imply uniform comparison of every positively rescaled closed graph.

theorem norm_prepared_rescaledGraphProjection_sub_le
    (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