OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CalibrationMesh.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Exact compatibility between polynomial hopping amplification and the equal masses of the unit-nucleus Gauss mesh.

  1. def OAI.ContinuumCoulomb.CalibrationMesh.base line 10
  2. def OAI.ContinuumCoulomb.CalibrationMesh.radius line 11
  3. def OAI.ContinuumCoulomb.CalibrationMesh.mesh line 12
  4. def OAI.ContinuumCoulomb.CalibrationMesh.width line 13
  5. def OAI.ContinuumCoulomb.CalibrationMesh.horizontal line 14
  6. def OAI.ContinuumCoulomb.CalibrationMesh.prefactor line 15
  7. def OAI.ContinuumCoulomb.CalibrationMesh.amplification line 16
  8. theorem OAI.ContinuumCoulomb.CalibrationMesh.prefactor_positive line 18
  9. theorem OAI.ContinuumCoulomb.CalibrationMesh.base_ge_two line 22
  10. theorem OAI.ContinuumCoulomb.CalibrationMesh.mesh_positive line 25
  11. theorem OAI.ContinuumCoulomb.CalibrationMesh.base_power_eq_mesh_cube line 27
  12. theorem OAI.ContinuumCoulomb.CalibrationMesh.amplification_eq_mesh line 32
  13. theorem OAI.ContinuumCoulomb.CalibrationMesh.physical_factor_eq line 39
  14. theorem OAI.ContinuumCoulomb.CalibrationMesh.amplification_positive line 44
  15. theorem OAI.ContinuumCoulomb.CalibrationMesh.mesh_eq_radius line 50
  16. theorem OAI.ContinuumCoulomb.CalibrationMesh.width_eq_radius line 55