OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/SlabBoxSchedule.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Rational slab dimensions with separate unary magnitude bounds. This covers exactly the half-cell boundary of the odd centered grid.

  1. abbrev OAI.ContinuumCoulomb.SlabBoxSchedule.Input line 11
  2. def OAI.ContinuumCoulomb.SlabBoxSchedule.input line 13
  3. def OAI.ContinuumCoulomb.SlabBoxSchedule.value line 19
  4. def OAI.ContinuumCoulomb.SlabBoxSchedule.bound line 21
  5. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.bound_mono line 25
  6. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.error line 32
  7. def OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth line 57

    Source documentation

    Exact half-width of the slab covered by centered indices from -q to q.

    def centeredWidth (q N : ℕ) : ℚ := ((q:ℚ)+1/2)/N
  8. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth_nonnegative line 59
  9. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth_le line 63
  10. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth_real line 70
  11. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth_product line 74
  12. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centeredWidth_product_bounds line 80
  13. def OAI.ContinuumCoulomb.SlabBoxSchedule.centered line 89
  14. theorem OAI.ContinuumCoulomb.SlabBoxSchedule.centered_error line 92