OAI/Analysis/HardSphere/Orbitals/Bump.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.CellOrbital.bump line 22
  2. def OAI.HardSphere.CellOrbital.centerLift line 25
  3. lemma OAI.HardSphere.CellOrbital.centerLift_coe line 28
  4. lemma OAI.HardSphere.CellOrbital.bump_project line 33
  5. lemma OAI.HardSphere.CellOrbital.bump_smooth line 41
  6. def OAI.HardSphere.CellOrbital.raw line 48
  7. lemma OAI.HardSphere.CellOrbital.bump_continuous line 51
  8. lemma OAI.HardSphere.CellOrbital.bump_bounds line 57
  9. lemma OAI.HardSphere.CellOrbital.bump_eq_one line 63
  10. lemma OAI.HardSphere.CellOrbital.bump_eq_zero line 75
  11. lemma OAI.HardSphere.CellOrbital.bump_support line 79
  12. lemma OAI.HardSphere.CellOrbital.box_volume_eq line 88
  13. def OAI.HardSphere.CellOrbital.mass line 97
  14. lemma OAI.HardSphere.CellOrbital.mass_lower line 99
  15. lemma OAI.HardSphere.CellOrbital.mass_pos line 111
  16. lemma OAI.HardSphere.CellOrbital.raw_fderiv line 114
  17. lemma OAI.HardSphere.CellOrbital.raw_partial line 135
  18. lemma OAI.HardSphere.CellOrbital.raw_partial_sq_le line 144
  19. lemma OAI.HardSphere.CellOrbital.raw_partial_zero line 154
  20. lemma OAI.HardSphere.CellOrbital.raw_energy_le line 164
  21. def OAI.HardSphere.CellOrbital.normalized line 193
  22. lemma OAI.HardSphere.CellOrbital.normalized_real line 197
  23. lemma OAI.HardSphere.CellOrbital.normalized_norm_sq line 201
  24. lemma OAI.HardSphere.CellOrbital.normalized_mass line 207
  25. lemma OAI.HardSphere.CellOrbital.normalized_support line 213
  26. lemma OAI.HardSphere.CellOrbital.normalized_bound line 224
  27. lemma OAI.HardSphere.CellOrbital.normalized_partial line 240
  28. lemma OAI.HardSphere.CellOrbital.normalized_energy_le line 248
  29. theorem OAI.HardSphere.CellOrbital.uniform_orbitals line 263