OAI/Analysis/ModularTheory/CompressedCorners.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Constructed traces, cpc retractions, and the resulting minimal tensor bound for the finite modular corners.

  1. def OAI.WeakPureInfiniteness.modularCornerToAbstract line 20
  2. lemma OAI.WeakPureInfiniteness.modularCornerToAbstract_injective line 62
  3. def OAI.WeakPureInfiniteness.modularCompressedTracialStateFormula line 70
  4. theorem OAI.WeakPureInfiniteness.exists_modularCompressedTracialState line 75
  5. def OAI.WeakPureInfiniteness.modularCompressedTracialState line 81

    Source documentation

    The constructed state is selected through its proved specification, so GNS instance reduction does not unfold the entire modular weight construction.

    def modularCompressedTracialState (S : StandardModularData H) (n : ℕ) :
    Pureness.TracialState (modularCompressedCorner S (n + 1)).toStarSubalgebra :=
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.modularCompressedCorner

  6. lemma OAI.WeakPureInfiniteness.modularCompressedTracialState_eq line 85
  7. lemma OAI.WeakPureInfiniteness.modularCompressedTracialState_faithful line 89
  8. theorem OAI.WeakPureInfiniteness.nuclear_quotient_modular_corner_expectation line 103