OAI/NumberTheory/Ostmann/Supply/AveragedKernelPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Averaging the actual tensor coordinates over summand elements

  1. def OAI.Ostmann.averagedCoordinates line 10
  2. theorem OAI.Ostmann.kernelPairing_sum_left line 14
  3. theorem OAI.Ostmann.kernelPairing_sum_right line 23
  4. theorem OAI.Ostmann.kernelPairing_const_mul line 33
  5. theorem OAI.Ostmann.kernelPairing_averages line 46