OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabOriginSchedule.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial unary precision choices for the finite-slab scalar.

  1. abbrev OAI.ContinuumCoulomb.SlabOriginSchedule.Input line 11
  2. def OAI.ContinuumCoulomb.SlabOriginSchedule.capDenominator line 13
  3. def OAI.ContinuumCoulomb.SlabOriginSchedule.boxWeight line 14
  4. def OAI.ContinuumCoulomb.SlabOriginSchedule.count line 15
  5. def OAI.ContinuumCoulomb.SlabOriginSchedule.input line 18
  6. def OAI.ContinuumCoulomb.SlabOriginSchedule.value line 22
  7. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.capDenominator_positive line 24
  8. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.boxWeight_positive line 28
  9. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.count_positive line 32
  10. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.dyadic_error line 37
  11. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.box_coefficient line 43
  12. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.numeric_budget line 53
  13. theorem OAI.ContinuumCoulomb.SlabOriginSchedule.error line 115