OAI/Analysis/CoulombRadii/SpectralTheory/AmbientEigen.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.massPair_congr line 13
  2. lemma OAI.Coulomb.formPair_congr line 22
  3. lemma OAI.Coulomb.massPair_symm line 28
  4. lemma OAI.Coulomb.formPair_symm line 30
  5. lemma OAI.Coulomb.massPair_rsmul_right line 32
  6. lemma OAI.Coulomb.formPair_rsmul_right line 34
  7. lemma OAI.Coulomb.massPair_rsmul_left line 40
  8. lemma OAI.Coulomb.formPair_rsmul_left line 42
  9. lemma OAI.Coulomb.massPair_permutation line 45
  10. lemma OAI.Coulomb.formPair_permutation line 54
  11. lemma OAI.Coulomb.massPair_finiteSum line 63
  12. lemma OAI.Coulomb.formPair_finiteSum line 69
  13. lemma OAI.Coulomb.sector_minimizer_ambient_eigen line 93
  14. lemma OAI.Coulomb.inner_double_real line 146
  15. lemma OAI.Coulomb.weighted_core_inequality line 151