OAI/MathematicalPhysics/Coulomb/OuterRadius.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombAtoms.Position line 15
  2. abbrev OAI.CoulombAtoms.Configuration line 18
  3. abbrev OAI.CoulombAtoms.SpinConfiguration line 21
  4. abbrev OAI.CoulombAtoms.WaveFunction line 23
  5. def OAI.CoulombAtoms.coordinateVector line 26
  6. def OAI.CoulombAtoms.permutationSign line 30
  7. structure OAI.CoulombAtoms.FormState line 35
  8. def OAI.CoulombAtoms.normSq line 49
  9. def OAI.CoulombAtoms.kineticEnergy line 53
  10. def OAI.CoulombAtoms.nuclearPotential line 59
  11. def OAI.CoulombAtoms.pairPotential line 63
  12. def OAI.CoulombAtoms.atomicCoulombForm line 68
  13. def OAI.CoulombAtoms.IsNormalizedGroundState line 75
  14. def OAI.CoulombAtoms.density line 81
  15. def OAI.CoulombAtoms.exteriorMass line 88
  16. def OAI.CoulombAtoms.halfElectronRadius line 92
  17. def OAI.CoulombAtoms.outerRadius line 95
  18. lemma OAI.CoulombAtoms.integrable_cons line 100
  19. lemma OAI.CoulombAtoms.integral_cons line 108
  20. lemma OAI.CoulombAtoms.density_one line 118
  21. lemma OAI.CoulombAtoms.density_nonneg line 131
  22. lemma OAI.CoulombAtoms.density_integrable line 138
  23. lemma OAI.CoulombAtoms.integral_density line 147
  24. lemma OAI.CoulombAtoms.integral_density_of_normalized line 158
  25. lemma OAI.CoulombAtoms.measurableSet_exterior line 164
  26. lemma OAI.CoulombAtoms.exteriorMass_nonneg line 167
  27. lemma OAI.CoulombAtoms.exteriorMass_antitone line 171
  28. lemma OAI.CoulombAtoms.halfElectronRadius_le line 178
  29. lemma OAI.CoulombAtoms.halfElectronRadius_bounds_of_tails line 184
  30. lemma OAI.CoulombAtoms.norm_ne_ae line 195
  31. lemma OAI.CoulombAtoms.exteriorMass_eq_ge line 202
  32. lemma OAI.CoulombAtoms.exteriorMass_zero line 208
  33. lemma OAI.CoulombAtoms.norm_exterior_indicator_le line 215
  34. lemma OAI.CoulombAtoms.exteriorMass_tendsto_zero line 221
  35. lemma OAI.CoulombAtoms.exteriorMass_continuous line 238
  36. lemma OAI.CoulombAtoms.exists_exteriorMass_le_half line 266
  37. lemma OAI.CoulombAtoms.exists_pos_exteriorMass_gt_half line 272
  38. lemma OAI.CoulombAtoms.halfElectronRadius_pos line 284
  39. lemma OAI.CoulombAtoms.outerRadius_pos line 293
  40. lemma OAI.CoulombAtoms.halfElectronRadius_mem line 301
  41. lemma OAI.CoulombAtoms.halfElectronRadius_le_iff line 307
  42. lemma OAI.CoulombAtoms.lt_halfElectronRadius_iff line 315
  43. lemma OAI.CoulombAtoms.exteriorMass_halfElectronRadius line 322
  44. lemma OAI.CoulombAtoms.exteriorMass_outerRadius line 340
  45. lemma OAI.CoulombAtoms.halfElectronRadius_bounds_of_compact_family line 349