OAI/NumberTheory/Ostmann/Supply/FiniteCoordinateEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The energy of averaged finite tensor coordinates

  1. theorem OAI.Ostmann.kernelPairing_identity line 11
  2. theorem OAI.Ostmann.averagedCoordinates_inner line 17
  3. theorem OAI.Ostmann.countingVectorNorm_sq_complex line 25
  4. theorem OAI.Ostmann.productVector_inner line 32
  5. def OAI.Ostmann.centeredSubsetVector line 39
  6. def OAI.Ostmann.centeredSubsetEnergy line 44
  7. theorem OAI.Ostmann.centeredSubsetEnergy_formula line 49
  8. theorem OAI.Ostmann.centeredSubsetEnergy_nonneg line 76
  9. theorem OAI.Ostmann.centeredSubsetEnergy_empty line 81