OAI/Analysis/CoulombIonization/FormDomain/CoulombCoercivity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.weakGraph_norm_sq line 16
  2. lemma OAI.CoulombAtom.fermionGraphValue_apply line 24
  3. lemma OAI.CoulombAtom.fermionGraph_norm_sq line 27
  4. lemma OAI.CoulombAtom.graphNuclear_bound line 37
  5. lemma OAI.CoulombAtom.graphValue_norm_sq line 55
  6. lemma OAI.CoulombAtom.nuclear_sum_arithmetic line 62
  7. lemma OAI.CoulombAtom.graphNuclear_sum_bound line 72
  8. lemma OAI.CoulombAtom.coulombFormOperator_inner_lower line 85
  9. lemma OAI.CoulombAtom.coercivity_arithmetic line 109
  10. lemma OAI.CoulombAtom.coulombFormOperator_coercive_bound line 113
  11. def OAI.CoulombAtom.shiftedCoulombFormOperator line 120
  12. lemma OAI.CoulombAtom.shiftedCoulombFormOperator_selfAdjoint line 124
  13. lemma OAI.CoulombAtom.shiftedCoulombFormOperator_inner line 132
  14. theorem OAI.CoulombAtom.shiftedCoulombFormOperator_coercive line 140
  15. lemma OAI.CoulombAtom.fermionPermutation_ae line 147
  16. lemma OAI.CoulombAtom.mem_fermionSpace_ae line 159
  17. lemma OAI.CoulombAtom.graphFormVector_admissible line 179
  18. def OAI.CoulombAtom.admissibleWeakGraph line 197
  19. lemma OAI.CoulombAtom.admissibleWeakGraph_value line 208
  20. lemma OAI.CoulombAtom.admissibleWeakGraph_gradient line 211
  21. def OAI.CoulombAtom.admissibleGraph line 216
  22. lemma OAI.CoulombAtom.graphFormVector_admissibleGraph_value line 229
  23. lemma OAI.CoulombAtom.graphFormVector_admissibleGraph_gradient line 235
  24. lemma OAI.CoulombAtom.admissibleGraph_norm line 241
  25. lemma OAI.CoulombAtom.formEnergy_congr_ae line 255
  26. theorem OAI.CoulombAtom.full_form_value_set line 297