OAI/Analysis/CoulombIonization/FormDomain/FormBottom.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.formLift line 16
  2. lemma OAI.CoulombAtom.formLift_eq line 20
  3. lemma OAI.CoulombAtom.formLift_inner line 25
  4. lemma OAI.CoulombAtom.formResolvent_apply line 30
  5. lemma OAI.CoulombAtom.formLift_self line 34
  6. lemma OAI.CoulombAtom.formResolvent_positive line 39
  7. lemma OAI.CoulombAtom.coercive_nonneg line 50
  8. lemma OAI.CoulombAtom.hermitian_quadratic_sub line 54
  9. lemma OAI.CoulombAtom.bounded_quadratic_upper line 68
  10. lemma OAI.CoulombAtom.injective_norm_pos line 76
  11. lemma OAI.CoulombAtom.form_reciprocal_resolvent_bound line 85
  12. lemma OAI.CoulombAtom.resolvent_norm_le_of_form_bound line 111
  13. lemma OAI.CoulombAtom.form_lower_of_unit line 132
  14. lemma OAI.CoulombAtom.denseRange_exists_nonzero line 152
  15. theorem OAI.CoulombAtom.form_infimum_eq_reciprocal line 159