OAI/Analysis/ModularTheory/WeightMonotone.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of the actual finite cutoff functionals on the positive modular core. The proof uses interval-projection commutation, not an assumed trace or a commutation rule for arbitrary operators on scalar L².

  1. lemma OAI.WeakPureInfiniteness.modularWeightCutoffVector_project line 18
  2. theorem OAI.WeakPureInfiniteness.modularCoreCutoffFunctional_mono line 36