OAI/Analysis/ModularTheory/CutoffTotality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete cutoff orbits are total in the modular Hilbert space. This supplies the density needed when gluing finite tracial corners.

  1. lemma OAI.WeakPureInfiniteness.modularCutoff_annihilator_scalar line 19
  2. lemma OAI.WeakPureInfiniteness.modularCutoff_annihilator_eq_zero line 64
  3. lemma OAI.WeakPureInfiniteness.modularFiniteCorner_annihilator_eq_zero line 116

    Source documentation

    The positive-size supported corners already have total cutoff orbits.

    lemma modularFiniteCorner_annihilator_eq_zero (S : StandardModularData H)
    (T : Lp H 2 (volume : Measure ℝ) →L[ℂ] K)
    (hz : ∀ n (a : Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ)),
      a ∈ modularCrossedProduct volume S →
      T ((modularFiniteProjection (H := H) (n + 1) * a * modularFiniteProjection (H := H) (n + 1))
…

    Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularFiniteProjection