OAI/Probability/InvariantIsing/Haar/HaarPolynomialKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite polynomial averaging kernels on the actual special orthogonal group.

  1. def OAI.InvariantIsing.haarKernelAtom line 12
  2. def OAI.InvariantIsing.haarKernelBase line 16
  3. def OAI.InvariantIsing.haarKernelAverage line 20
  4. lemma OAI.InvariantIsing.continuous_haarKernelAtom line 25
  5. lemma OAI.InvariantIsing.haarKernelBase_sum line 33
  6. theorem OAI.InvariantIsing.haarKernelAverage_value line 46