OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceZeroFilter.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual deletion of zero source bonds after common-denominator rounding.

  1. def OAI.ContinuumCoulomb.SourceZeroFilter.keep line 10
  2. def OAI.ContinuumCoulomb.SourceZeroFilter.step line 12
  3. theorem OAI.ContinuumCoulomb.SourceZeroFilter.fold_step line 14
  4. theorem OAI.ContinuumCoulomb.SourceZeroFilter.filter_code_le line 26
  5. def OAI.ContinuumCoulomb.SourceZeroFilter.isZero line 39
  6. def OAI.ContinuumCoulomb.SourceZeroFilter.stepProgram line 45
  7. def OAI.ContinuumCoulomb.SourceZeroFilter.foldProgram line 54
  8. def OAI.ContinuumCoulomb.SourceZeroFilter.filterProgram line 65
  9. theorem OAI.ContinuumCoulomb.SourceZeroFilter.nonzero_mem line 72