OAI/Analysis/CoulombRadii/FormDomain/ParticleGradientNorm.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.oneParticleGradientNorm line 12
  2. theorem OAI.NeutralAtom.gradientNormSquared_insert line 15
  3. theorem OAI.NeutralAtom.weighted_normSquared_insert line 26
  4. theorem OAI.NeutralAtom.potentialForm_insert_le line 40
  5. theorem OAI.NeutralAtom.energy_insert_le line 88
  6. def OAI.NeutralAtom.distantCenter line 101
  7. theorem OAI.NeutralAtom.distantCenter_norm line 103
  8. theorem OAI.NeutralAtom.bindingBump_smooth line 106
  9. def OAI.NeutralAtom.distantMass line 108
  10. theorem OAI.NeutralAtom.distantMass_pos line 110
  11. def OAI.NeutralAtom.distantPacket line 124
  12. theorem OAI.NeutralAtom.distantPacket_smooth line 127
  13. theorem OAI.NeutralAtom.distantPacket_compact line 131
  14. theorem OAI.NeutralAtom.distantPacket_memLp line 138
  15. theorem OAI.NeutralAtom.distantPacket_derivative_memLp line 141
  16. theorem OAI.NeutralAtom.integral_distant_comp line 146
  17. theorem OAI.NeutralAtom.distantPacket_normalized line 153
  18. theorem OAI.NeutralAtom.distantPacket_zero line 161
  19. theorem OAI.NeutralAtom.distantPacket_derivative_zero line 173
  20. theorem OAI.NeutralAtom.distantPacket_fderiv line 182
  21. theorem OAI.NeutralAtom.distantPacket_gradientNorm line 196
  22. theorem OAI.NeutralAtom.distantInsertion_error_tendsto line 208
  23. theorem OAI.NeutralAtom.FormDomain.exists_inserted_trial line 219
  24. theorem OAI.NeutralAtom.FormDomain.exists_successor_trial line 259
  25. def OAI.NeutralAtom.sectorEnergy line 269
  26. def OAI.NeutralAtom.unrestrictedEnergy line 273
  27. theorem OAI.NeutralAtom.unrestrictedEnergy_le_sector line 275
  28. theorem OAI.NeutralAtom.sectorEnergy_le_trial line 278
  29. theorem OAI.NeutralAtom.sectorEnergy_succ_le line 282
  30. theorem OAI.NeutralAtom.sectorEnergy_antitone line 293
  31. theorem OAI.NeutralAtom.groundState_energy_eq_sector line 296
  32. def OAI.NeutralAtom.vacuumWavefunction line 306
  33. def OAI.NeutralAtom.vacuumGradient line 308
  34. theorem OAI.NeutralAtom.vacuum_volume_univ line 310
  35. theorem OAI.NeutralAtom.vacuum_formDomain line 314
  36. theorem OAI.NeutralAtom.vacuum_normalized line 331
  37. theorem OAI.NeutralAtom.energy_vacuum_sector line 335
  38. theorem OAI.NeutralAtom.sectorEnergy_vacuum line 338
  39. theorem OAI.NeutralAtom.sectorEnergy_nonpos line 346
  40. theorem OAI.NeutralAtom.sectorEnergy_finite_of_neutral_groundState line 349
  41. def OAI.NeutralAtom.UniformPredecessorOffset line 361
  42. theorem OAI.NeutralAtom.first_ionization_le_of_predecessor_offset line 365
  43. def OAI.NeutralAtom.firstIonization line 380
  44. theorem OAI.NeutralAtom.bounded_firstIonization_of_uniformPredecessorOffset line 383