OAI/Analysis/ModularTheory/NormalAdjointWeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Adjoint-weight symmetry for a normal-ordered core element. Both bounds come from actual Gaussian regularizations: closedness gives one direction, and right-multiplier contractivity gives the reverse direction.

  1. lemma OAI.WeakPureInfiniteness.modularNormalOrdered_adjoint_weight line 19