OAI/Analysis/ModularTheory/KernelIdentification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Identification of integrated covariant kernels with bounded Gaussian regularizations of the actual convolution-smoothed fixed point.

  1. def OAI.WeakPureInfiniteness.weightedScalarSliceKernel line 19
  2. lemma OAI.WeakPureInfiniteness.weightedScalarSliceKernel_integrable line 24
  3. lemma OAI.WeakPureInfiniteness.characterWeightedKernel_integrable line 33
  4. theorem OAI.WeakPureInfiniteness.gaussianSmoothedKernel_pairing line 45
  5. lemma OAI.WeakPureInfiniteness.gaussianWeightedKernel_integrable line 83
  6. lemma OAI.WeakPureInfiniteness.gaussianSchurFactor_star_integrable line 95
  7. theorem OAI.WeakPureInfiniteness.integratedGaussianKernel_pairing line 103
  8. lemma OAI.WeakPureInfiniteness.operator_eq_of_integrable_scalar_pairs line 126
  9. theorem OAI.WeakPureInfiniteness.modularKernelRegularization_eq_dualAverage line 158