OAI/Analysis/ModularTheory/DualKernelPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact character factor on a convolution-smoothed kernel under the dual action. This precedes Gaussian integration of that factor.

  1. lemma OAI.WeakPureInfiniteness.modularDual_scalar_integrable line 15
  2. lemma OAI.WeakPureInfiniteness.modularDual_scalarVector line 25
  3. lemma OAI.WeakPureInfiniteness.modularDual_inner_left line 36
  4. lemma OAI.WeakPureInfiniteness.spectralCharacter_dual_kernel line 40
  5. theorem OAI.WeakPureInfiniteness.modularDual_convolutionSmoothed_pairing line 51