OAI/Analysis/CoulombRadii/FormDomain/RegularizedHardyField.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.regularizedHardyField line 14
  2. lemma OAI.Coulomb.contDiff_regularizedHardyField line 18
  3. lemma OAI.Coulomb.fderiv_regularizedHardyField line 24
  4. lemma OAI.Coulomb.regularizedHardyField_sq_sum line 45
  5. lemma OAI.Coulomb.regularizedHardyField_divergence line 52
  6. lemma OAI.Coulomb.regularizedHardyField_weight line 68
  7. lemma OAI.Coulomb.integrable_smooth_mul_compact_deriv line 81
  8. lemma OAI.Coulomb.integrable_smooth_deriv_mul_compact line 87
  9. lemma OAI.Coulomb.integral_compact_ibp line 93
  10. lemma OAI.Coulomb.smooth_square_fderiv line 104
  11. lemma OAI.Coulomb.integral_compact_ibp_deriv_form line 111
  12. lemma OAI.Coulomb.integral_compact_ibp_square line 121
  13. lemma OAI.Coulomb.hardy_pointwise_algebra line 136
  14. lemma OAI.Coulomb.regularizedHardy_pointwise line 161
  15. lemma OAI.Coulomb.integrable_compact_deriv_sq line 175
  16. lemma OAI.Coulomb.integrable_compact_ibp_square line 185
  17. lemma OAI.Coulomb.integral_hardy_algebra line 198
  18. lemma OAI.Coulomb.integrable_compact_regularized_weight line 216
  19. lemma OAI.Coulomb.smooth_compact_regularized_hardy line 227
  20. lemma OAI.Coulomb.nonneg_fatou_integrable line 251
  21. lemma OAI.Coulomb.smooth_compact_hardy line 284
  22. lemma OAI.Coulomb.convolution_sq_le line 328
  23. lemma OAI.Coulomb.convolution_sq_integral_le line 361
  24. lemma OAI.Coulomb.real_convolution_comm line 386
  25. lemma OAI.Coulomb.fderiv_const_sub_comp line 393
  26. lemma OAI.Coulomb.weak_convolution_partial line 402
  27. lemma OAI.Coulomb.ae_nonneg_fatou_integrable line 423