PreparedRightGraphBridge.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Prepared graph comparison from common right actions

The vector and conjugation identities are imposed only on the shared increasing matrix algebra. In particular, no tracial state on either ambient algebra is needed. The relative right-action data imply the required centralizer identities, and matrix averaging transfers relative irreducibility to the nearby algebra.

theorem OAI.KadisonKastler.vector_functional_centralizes_of_commonRight line 33

Source documentation

Right multiplication on the common algebra implies centralization of the vector functional, without any trace hypothesis on the ambient algebra.

theorem vector_functional_centralizes_of_commonRight
    (R N : VonNeumannAlgebra H) (hRN : R ≤ N)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H)
    (hright : ∀ r ∈ R, conjugationOperator J r ∈ N.commutant)
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω)
    (r : Algebra R) (x : Algebra N) :
    inner ℂ Ω ((r.val * x.val) Ω) = inner ℂ Ω ((x.val * r.val) Ω) := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.commonRightAlgebra_le_commutant line 47

Source documentation

The source right algebra commutes with the common left algebra.

theorem commonRightAlgebra_le_commutant
    (M R S : VonNeumannAlgebra H) (hRM : R ≤ M) (J : H ≃ₗᵢ⋆[ℂ] H)
    (hrightM : ∀ r ∈ R, conjugationOperator J r ∈ M.commutant)
    (hS : (S : Set (H →L[ℂ] H)) =
      conjugationOperator J '' (R : Set (H →L[ℂ] H))) :
    S ≤ R.commutant := by
…

Mentions: OAI.KadisonKastler.conjugationOperator

theorem OAI.KadisonKastler.norm_preparedRight_graphProjection_sub_le line 63

Source documentation

Common right-action data on R suffice for uniform rescaled graph comparison. The ambient algebras need not carry tracial vector states.

theorem norm_preparedRight_graphProjection_sub_le
    (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.norm_preparedRight_graphProjection_sub_le_of_right_algebra line 129

Source documentation

Literal containment of the common right algebra is the only neighbor right-action premise needed for the graph estimate.

theorem norm_preparedRight_graphProjection_sub_le_of_right_algebra
    (M N R S : 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)
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω)
…

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

theorem OAI.KadisonKastler.norm_corrected_preparedRight_graphProjection_sub_le line 161

Source documentation

A supplied localized correction gives the generic, possibly nontracial, prepared graph estimate with its exact ordinary-gap cost.

theorem norm_corrected_preparedRight_graphProjection_sub_le
    (M N R S : 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))
    (hrightM : ∀ r ∈ R, conjugationOperator J r ∈ M.commutant)
    (hvector : ∀ r ∈ R, conjugationOperator J (star r) Ω = r Ω)
    (hS : (S : Set (H →L[ℂ] H)) =
…

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

theorem OAI.KadisonKastler.exists_preparedRight_graph_comparison line 199
Source documentation
The localized embedding chooses the second correction from the genuine relative right-action data. No trace on M or N is assumed.
```
theorem exists_preparedRight_graph_comparison
    (hpub : PublishedLocalizedAmenableEmbedding (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedLocalizedAmenableEmbedding