OAI/Analysis/ModularTheory/CornerRepresentedBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-tracial bound for the actual modular-corner operators.

  1. lemma OAI.WeakPureInfiniteness.modularCornerProduct_gnsSupport line 17
  2. abbrev OAI.WeakPureInfiniteness.nuclear_quotient_modular_corner_represented_bound line 32

    Source documentation

    The concrete bound is the direct specialization of the represented finite-tracial bound, with its canonical GNS structures kept intact.

    abbrev nuclear_quotient_modular_corner_represented_bound
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ atTop)
    (hA : Nuclear A) (q : A →⋆ₐ[ℂ] B) (hq : Function.Surjective q)
    (π : B →⋆ₐ[ℂ] (H →L[ℂ] H)) (S : StandardModularData H)
    (hS : S.M = bicommutant π.range) (n : ℕ) {I : Type*} [Fintype I]
    (a b : I → (modularCompressedCorner S (n + 1)).toStarSubalgebra) :=
…

    Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.modularCompressedCorner