OAI/Analysis/CoulombIonization/Variational/BindingBase.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.linear_hardy_bound line 16
  2. lemma OAI.CoulombAtom.sectorGraphPermutation_fixed line 40
  3. lemma OAI.CoulombAtom.sectorGraphPermutation_component line 46
  4. lemma OAI.CoulombAtom.complex_sign_norm line 52
  5. lemma OAI.CoulombAtom.graphComponent_permutation_norm line 58
  6. lemma OAI.CoulombAtom.graphComponent_permutation_integral line 76
  7. lemma OAI.CoulombAtom.sum_spins_permutation line 88
  8. lemma OAI.CoulombAtom.graphComponent_permutation_sum_integral line 97
  9. def OAI.CoulombAtom.quantumEnergyDensity line 107
  10. lemma OAI.CoulombAtom.SobolevFermion.quantumEnergyDensity_integrable line 113
  11. lemma OAI.CoulombAtom.formEnergy_eq_density line 131
  12. def OAI.CoulombAtom.quantumCoreDensity line 176
  13. lemma OAI.CoulombAtom.SobolevFermion.quantumCoreDensity_integrable line 183
  14. def OAI.CoulombAtom.exteriorCoordinates line 206
  15. lemma OAI.CoulombAtom.exteriorCoordinates_join line 209
  16. lemma OAI.CoulombAtom.exteriorCoordinates_continuous line 214
  17. lemma OAI.CoulombAtom.weighted_integral_join line 219
  18. lemma OAI.CoulombAtom.weighted_sum_integral_join line 232
  19. lemma OAI.CoulombAtom.quantumCoreDensity_last line 246
  20. lemma OAI.CoulombAtom.coreSlice_energy_weighted_reconstruction line 259
  21. lemma OAI.CoulombAtom.coreSlice_mass_weighted_reconstruction line 273
  22. lemma OAI.CoulombAtom.weighted_core_last line 280
  23. lemma OAI.CoulombAtom.graphFormVector_value_eq line 290
  24. lemma OAI.CoulombAtom.graphFormVector_gradient_eq line 293
  25. lemma OAI.CoulombAtom.sum_excluding_perm line 299
  26. lemma OAI.CoulombAtom.sum_pairs_excluding_perm line 305
  27. lemma OAI.CoulombAtom.quantumCoreDensity_reindex line 316
  28. lemma OAI.CoulombAtom.graphFormVector_permutation_norm line 329
  29. lemma OAI.CoulombAtom.quantumCoreDensity_permutation line 345
  30. lemma OAI.CoulombAtom.weighted_core_permutation line 353
  31. lemma OAI.CoulombAtom.weighted_core_coordinate line 367
  32. lemma OAI.CoulombAtom.sum_excluding_add line 389
  33. lemma OAI.CoulombAtom.pairs_excluding_add line 396
  34. lemma OAI.CoulombAtom.quantumEnergyDensity_delete line 415