OAI/Analysis/ModularTheory/CoreTracial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Tracial symmetry of the constructed modular-core square weight. Finite two-vector approximations suffice; no norm-bounded density theorem or traciality assumption is used.

  1. lemma OAI.WeakPureInfiniteness.core_twoVector_sequence line 19
  2. lemma OAI.WeakPureInfiniteness.modularCore_regularized_adjoint_weight_le line 44
  3. lemma OAI.WeakPureInfiniteness.modularCoreSquareWeight_le_of_strong_bound line 82
  4. lemma OAI.WeakPureInfiniteness.frequencyGaussian_selfAdjoint line 97
  5. lemma OAI.WeakPureInfiniteness.core_adjoint_weight_le line 103
  6. theorem OAI.WeakPureInfiniteness.modularCoreSquareWeight_adjoint line 120

    Source documentation

    The actual extended square weight of the modular core is tracial. The statement includes infinite weight and requires no extra trace hypothesis.

    theorem modularCoreSquareWeight_adjoint (S : StandardModularData H)
    (T : Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ))
    (hT : T ∈ modularCrossedProduct (volume : Measure ℝ) S) :
    modularCoreSquareWeight S (star T) = modularCoreSquareWeight S T := by
…

    Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularCoreSquareWeight