OAI/MathematicalPhysics/ContinuumCoulomb/Programs/CenteredGaussProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal polynomial generation of the complete rectangular Gauss-label list. The three integer radii are unary, so the cubic number of output cells is polynomial in the encoded input size.

  1. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.flatten_code_bound line 13
  2. theorem OAI.ContinuumCoulomb.CenteredGaussLabels.fold_append line 22
  3. def OAI.ContinuumCoulomb.CenteredGaussLabels.flattenProgram line 28
  4. def OAI.ContinuumCoulomb.CenteredGaussLabels.productProgram line 46
  5. def OAI.ContinuumCoulomb.CenteredGaussLabels.radiiCode line 57
  6. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.integerStep line 59
  7. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.integersProgram line 66
  8. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.firstRadiusProgram line 73
  9. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.tailRadiiProgram line 75
  10. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.secondRadiusProgram line 77
  11. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.thirdRadiusProgram line 79
  12. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.cellsProgram line 82
  13. opaque OAI.ContinuumCoulomb.CenteredGaussLabels.labelsProgram line 88
  14. def OAI.ContinuumCoulomb.CenteredGaussLabels.labelsCertificate line 93