OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CenteredGaussEquiv.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The emitted centered label list is exactly the finite cell-by-eight-node grid used by the Coulomb quadrature theorems.

  1. def OAI.ContinuumCoulomb.CenteredGaussLabels.decode line 12
  2. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.bit_value line 15
  3. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.index_decode line 18
  4. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.decode_index line 26
  5. def OAI.ContinuumCoulomb.CenteredGaussLabels.indexEquiv line 31
  6. abbrev OAI.ContinuumCoulomb.CenteredGaussLabels.Grid line 37
  7. def OAI.ContinuumCoulomb.CenteredGaussLabels.restrictedEquiv line 40
  8. def OAI.ContinuumCoulomb.CenteredGaussLabels.enumerationEquiv line 54
  9. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.enumeration_first line 57
  10. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.enumeration_second line 60
  11. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.sum_enumeration line 63