OAI/Analysis/CoulombIonization/FormDomain/WeakDirectionalDerivative.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAtom.HasWeakDirectionalDerivative line 19
  2. def OAI.CoulombAtom.testBump line 24
  3. def OAI.CoulombAtom.testScale line 30
  4. def OAI.CoulombAtom.testCutoff line 32
  5. lemma OAI.CoulombAtom.testScale_pos line 34
  6. lemma OAI.CoulombAtom.testScale_le_one line 35
  7. lemma OAI.CoulombAtom.testScale_tendsto line 38
  8. lemma OAI.CoulombAtom.testCutoff_smooth line 43
  9. lemma OAI.CoulombAtom.testCutoff_compact line 47
  10. lemma OAI.CoulombAtom.testCutoff_norm_le line 52
  11. lemma OAI.CoulombAtom.testCutoff_tendsto line 58
  12. lemma OAI.CoulombAtom.testCutoff_derivative line 65
  13. lemma OAI.CoulombAtom.testCutoff_derivative_control line 76
  14. lemma OAI.CoulombAtom.fderiv_mul_real line 93
  15. lemma OAI.CoulombAtom.weak_derivative_smooth_L2 line 103
  16. lemma OAI.CoulombAtom.fderiv_schwartz_postcomp line 160
  17. lemma OAI.CoulombAtom.weak_derivative_schwartz line 165
  18. lemma OAI.CoulombAtom.weak_derivative_tempered line 216
  19. lemma OAI.CoulombAtom.weak_fourier_derivative_ae line 236
  20. lemma OAI.CoulombAtom.l2_norm_sq_integral line 268
  21. lemma OAI.CoulombAtom.weak_fourier_moment line 277
  22. lemma OAI.CoulombAtom.weak_fourier_kinetic line 301
  23. lemma OAI.CoulombAtom.classical_fourier_continuous line 320
  24. lemma OAI.CoulombAtom.integral_fourier_mul line 325
  25. lemma OAI.CoulombAtom.l2_fourier_ae_classical line 337
  26. lemma OAI.CoulombAtom.integrable_mul_real_test line 360
  27. lemma OAI.CoulombAtom.weak_derivative_mul_cutoff line 366
  28. lemma OAI.CoulombAtom.complex_schwartz_shift_memLp line 408
  29. lemma OAI.CoulombAtom.weak_window_memLp line 413
  30. lemma OAI.CoulombAtom.weak_window_integrable line 417
  31. lemma OAI.CoulombAtom.weak_window_derivative line 421