OAI/Analysis/CoulombIonization/RadialBounds/SquareCompletion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.derivative_norm_sq line 16
  2. lemma OAI.CoulombAtom.square_completion_pointwise line 23
  3. lemma OAI.CoulombAtom.square_completion_integral line 36
  4. lemma OAI.CoulombAtom.square_completion_bound line 79
  5. lemma OAI.CoulombAtom.integrable_norm_sq_derivative line 126
  6. lemma OAI.CoulombAtom.square_completion_integral_of_memLp line 137
  7. lemma OAI.CoulombAtom.square_completion_bound_of_memLp line 177
  8. def OAI.CoulombAtom.regularizedRadius line 227
  9. def OAI.CoulombAtom.radialField line 229
  10. lemma OAI.CoulombAtom.regularizedRadius_pos line 231
  11. lemma OAI.CoulombAtom.regularizedRadius_sq line 236
  12. lemma OAI.CoulombAtom.regularizedRadius_smooth line 239
  13. lemma OAI.CoulombAtom.radialField_smooth line 245
  14. lemma OAI.CoulombAtom.radialField_fderiv line 250
  15. lemma OAI.CoulombAtom.sum_coordinate_sq line 269
  16. lemma OAI.CoulombAtom.coordinate_sq_le line 272
  17. lemma OAI.CoulombAtom.norm_le_regularizedRadius line 276
  18. lemma OAI.CoulombAtom.le_regularizedRadius line 281
  19. lemma OAI.CoulombAtom.radialField_norm_le line 287
  20. lemma OAI.CoulombAtom.sum_radialField_sq_le line 297
  21. lemma OAI.CoulombAtom.radialField_derivative_bounds line 304
  22. lemma OAI.CoulombAtom.radialField_divergence line 324
  23. def OAI.CoulombAtom.regularizedCoulomb line 346
  24. lemma OAI.CoulombAtom.regularizedCoulomb_nonneg line 349
  25. lemma OAI.CoulombAtom.regularizedCoulomb_le line 353
  26. lemma OAI.CoulombAtom.regularizedCoulomb_continuous line 362
  27. lemma OAI.CoulombAtom.coordinate_radialField_fderiv line 367