OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceCoefficientRounding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact common-denominator source coefficient rounding, implemented by actual integer/rational machine arithmetic. Nonzero rounded weights have an inverse-polynomial lower bound without assuming one for the source.

  1. def OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficient line 13
  2. theorem OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficient_error line 15
  3. theorem OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficient_nonzero_lower line 26
  4. theorem OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficient_upper line 41
  5. abbrev OAI.ContinuumCoulomb.SourceCoefficientRounding.Input line 51
  6. def OAI.ContinuumCoulomb.SourceCoefficientRounding.inputCode line 53
  7. def OAI.ContinuumCoulomb.SourceCoefficientRounding.mProgram line 55
  8. def OAI.ContinuumCoulomb.SourceCoefficientRounding.weightProgram line 57
  9. def OAI.ContinuumCoulomb.SourceCoefficientRounding.roundedProgram line 59
  10. def OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficientProgram line 62
  11. def OAI.ContinuumCoulomb.SourceCoefficientRounding.bondProgram line 66
  12. def OAI.ContinuumCoulomb.SourceCoefficientRounding.listProgram line 73