OAI/Analysis/ModularTheory/FieldPairing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The matrix coefficients of integrated modular fields, computed in the actual noncommutative L² representation.

  1. lemma OAI.WeakPureInfiniteness.modularFieldOperator_pairing line 17
  2. lemma OAI.WeakPureInfiniteness.integratedModularField_pairing line 39
  3. lemma OAI.WeakPureInfiniteness.modularKernelRegularization_pairing line 58