OAI/Analysis/OperatorAlgebra/ScalarKernelPairing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Matrix coefficients of the actual convolution-smoothed operator are the double integrals of its covariant scalar-slice kernel.

  1. lemma OAI.WeakPureInfiniteness.inner_integral_left line 17
  2. lemma OAI.WeakPureInfiniteness.inner_integral_pair line 25
  3. lemma OAI.WeakPureInfiniteness.scalarTranslationSynthesis_integrable line 37
  4. theorem OAI.WeakPureInfiniteness.scalarKernel_convolution_pairing line 47
  5. def OAI.WeakPureInfiniteness.convolutionSmoothedOperator line 71
  6. theorem OAI.WeakPureInfiniteness.convolutionSmoothedOperator_pairing line 78