OAI/Analysis/CoulombIonization/Variational/DiffuseSeed.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.diffuseSeed line 120
  2. def OAI.CoulombAtom.diffuseRaw line 122
  3. lemma OAI.CoulombAtom.diffuseSeed_smooth line 124
  4. lemma OAI.CoulombAtom.diffuseSeed_compact line 127
  5. lemma OAI.CoulombAtom.diffuseRaw_sobolev line 130
  6. lemma OAI.CoulombAtom.diffuseRaw_mass_pos line 141
  7. lemma OAI.CoulombAtom.diffuseRaw_gradient line 152
  8. lemma OAI.CoulombAtom.diffuseRaw_mass line 161
  9. lemma OAI.CoulombAtom.diffuseRaw_kinetic line 171
  10. lemma OAI.CoulombAtom.formKinetic_scale line 183
  11. def OAI.CoulombAtom.diffuseOrbital line 189
  12. lemma OAI.CoulombAtom.diffuseOrbital_admissible line 192
  13. def OAI.CoulombAtom.diffuseKinetic line 195
  14. lemma OAI.CoulombAtom.diffuseKinetic_nonneg line 198
  15. lemma OAI.CoulombAtom.diffuseOrbital_kinetic line 201
  16. lemma OAI.CoulombAtom.diffuseSeed_zero line 211
  17. lemma OAI.CoulombAtom.diffuseRaw_zero line 222
  18. lemma OAI.CoulombAtom.diffuseOrbital_zero line 233
  19. lemma OAI.CoulombAtom.tensorCross_le line 249
  20. lemma OAI.CoulombAtom.exterior_insertion_trial line 296
  21. theorem OAI.CoulombAtom.quantum_energy_succ_le line 319
  22. theorem OAI.CoulombAtom.quantum_energy_antitone line 337