OAI/Analysis/ModularTheory/NormalAdjoint.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The adjoint of a normal-ordered core element, regularized by the explicit Gaussian approximate identity. Its finite-weight vector is the actual Tomita Fourier vector, with no tracial identity assumed.

  1. lemma OAI.WeakPureInfiniteness.modularStarEnvelope line 17
  2. lemma OAI.WeakPureInfiniteness.modularAdjoint_halfGraph line 25
  3. def OAI.WeakPureInfiniteness.modularNormalAdjointRegularized line 29
  4. lemma OAI.WeakPureInfiniteness.modularNormalAdjoint_mem line 35
  5. lemma OAI.WeakPureInfiniteness.modularNormalAdjointRegularized_mem line 42
  6. lemma OAI.WeakPureInfiniteness.modularNormalAdjointRegularized_finite line 47
  7. lemma OAI.WeakPureInfiniteness.modularNormalAdjointRegularized_vector line 53
  8. lemma OAI.WeakPureInfiniteness.modularNormalAdjointRegularized_vector_tendsto line 75