OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourceNuclearProgram.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Raw-source assembly of the actual transported unit nuclei. The well scale is exactly lambda, the cutoff width is the exact centered slab width, and all three lattice radii come from the same powers as the thresholds.

  1. def OAI.ContinuumCoulomb.SourceNuclearProgram.sites line 13
  2. def OAI.ContinuumCoulomb.SourceNuclearProgram.amplification line 17
  3. def OAI.ContinuumCoulomb.SourceNuclearProgram.input line 20
  4. def OAI.ContinuumCoulomb.SourceNuclearProgram.nuclei line 28
  5. opaque OAI.ContinuumCoulomb.SourceNuclearProgram.amplificationProgram line 32
  6. opaque OAI.ContinuumCoulomb.SourceNuclearProgram.verticalProgram line 49
  7. opaque OAI.ContinuumCoulomb.SourceNuclearProgram.inputProgram line 59
  8. opaque OAI.ContinuumCoulomb.SourceNuclearProgram.program line 71
  9. def OAI.ContinuumCoulomb.SourceNuclearProgram.certificate line 76
  10. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.mesh line 81
  11. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.field_scale line 84
  12. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.field_width line 87
  13. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.field_sites line 90
  14. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.real_positions line 93
  15. theorem OAI.ContinuumCoulomb.SourceNuclearProgram.nuclei_length line 106