OAI/Analysis/CoulombIonization/FormDomain/WeakDerivative.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.IsWeakDerivative line 16
  2. lemma OAI.CoulombAtom.IsWeakDerivative.congr_ae line 21
  3. lemma OAI.CoulombAtom.IsWeakDerivative.unique line 31
  4. def OAI.CoulombAtom.l2Test line 40
  5. lemma OAI.CoulombAtom.l2Test_apply line 46
  6. lemma OAI.CoulombAtom.test_memLp line 56
  7. lemma OAI.CoulombAtom.test_deriv_memLp line 61
  8. abbrev OAI.CoulombAtom.WeakGraphAmbient line 77
  9. def OAI.CoulombAtom.weakGraphTest line 80
  10. def OAI.CoulombAtom.weakGraph line 88
  11. lemma OAI.CoulombAtom.mem_weakGraph line 93
  12. lemma OAI.CoulombAtom.weakGraph_isClosed line 98
  13. instance OAI.CoulombAtom.weakGraph_completeSpace line 103
  14. def OAI.CoulombAtom.weakGraphValue line 106
  15. lemma OAI.CoulombAtom.weakGraphValue_injective line 111
  16. lemma OAI.CoulombAtom.smooth_derivative_continuous line 131
  17. lemma OAI.CoulombAtom.compact_derivative line 135
  18. lemma OAI.CoulombAtom.smooth_complex_ofReal_derivative line 139
  19. lemma OAI.CoulombAtom.compact_norm_sq line 146
  20. lemma OAI.CoulombAtom.smooth_weak_gradient line 154
  21. def OAI.CoulombAtom.smoothGraph line 177
  22. lemma OAI.CoulombAtom.weakGraphValue_smoothGraph line 193
  23. lemma OAI.CoulombAtom.orthogonal_weakGraphValue_zero line 199
  24. theorem OAI.CoulombAtom.weakGraphValue_denseRange line 219