OAI/Analysis/CoulombIonization/FormDomain/CoherentSchwartz.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.coherentOverlap_continuous_schwartz line 17
  2. lemma OAI.CoulombAtom.coherentWindow_compact line 35
  3. lemma OAI.CoulombAtom.coherentOverlap_momentum_schwartz line 43
  4. lemma OAI.CoulombAtom.coherentOverlap_momentum_integrable_schwartz line 58
  5. lemma OAI.CoulombAtom.coherent_position_integrable_schwartz line 71
  6. lemma OAI.CoulombAtom.coherentOverlap_integrable_schwartz line 90
  7. lemma OAI.CoulombAtom.coherentOverlap_resolution_schwartz line 108
  8. lemma OAI.CoulombAtom.coherentVector_inner_schwartz line 124
  9. lemma OAI.CoulombAtom.schwartz_toLp_norm_sq line 133
  10. lemma OAI.CoulombAtom.coherentOverlap_measure_le_schwartz line 138
  11. lemma OAI.CoulombAtom.coherentOperator_schwartz_le line 152
  12. lemma OAI.CoulombAtom.coherentOperator_quadratic_le line 161
  13. lemma OAI.CoulombAtom.coherentOperator_one_sub_positive line 175