OAI/Analysis/CoulombIonization/Variational/CoulombNear.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAnalysis.coulombNear line 52
  2. def OAI.CoulombAnalysis.coulombFar line 53
  3. lemma OAI.CoulombAnalysis.coulombNear_memLp line 55
  4. lemma OAI.CoulombAnalysis.coulombFar_bound line 59
  5. lemma OAI.CoulombAnalysis.coulombFar_continuous line 63
  6. lemma OAI.CoulombAnalysis.coulomb_decompose line 67
  7. def OAI.CoulombAnalysis.tfSubMap line 75
  8. lemma OAI.CoulombAnalysis.tfSubMap_preserving line 76
  9. lemma OAI.CoulombAnalysis.tfSubMap_continuous line 79
  10. def OAI.CoulombAnalysis.coulombNearLp line 83
  11. def OAI.CoulombAnalysis.coulombNearTranslate line 85
  12. lemma OAI.CoulombAnalysis.coulombNearTranslate_coe line 88
  13. lemma OAI.CoulombAnalysis.coulombNearTranslate_continuous line 93
  14. lemma OAI.CoulombAnalysis.coulombNearMultiply_integrable line 97
  15. lemma OAI.CoulombAnalysis.coulombFarMultiply_integrable line 101
  16. lemma OAI.CoulombAnalysis.tfPotential_integrable line 106
  17. lemma OAI.CoulombAnalysis.tfPotential_continuous line 115
  18. def OAI.CoulombAnalysis.newtonMul line 148
  19. def OAI.CoulombAnalysis.newtonMul₁ line 149
  20. lemma OAI.CoulombAnalysis.fderiv_apply_const_scalar line 151
  21. lemma OAI.CoulombAnalysis.fderiv_convolution_eval line 157
  22. lemma OAI.CoulombAnalysis.second_fderiv_convolution line 167
  23. lemma OAI.CoulombAnalysis.second_kernel_integrable line 185
  24. lemma OAI.CoulombAnalysis.laplacian_convolution line 199
  25. def OAI.CoulombAnalysis.annularCoulomb line 208
  26. lemma OAI.CoulombAnalysis.annularCoulomb_compact line 211
  27. lemma OAI.CoulombAnalysis.annularCoulomb_smooth line 215
  28. lemma OAI.CoulombAnalysis.annularCoulomb_eq line 228
  29. lemma OAI.CoulombAnalysis.annularCoulomb_eventually line 233
  30. lemma OAI.CoulombAnalysis.annularCoulomb_laplacian line 239
  31. theorem OAI.CoulombAnalysis.tfPotential_harmonic_separated line 249
  32. lemma OAI.exists_orthogonal_map_norm_eq line 290