OAI/Analysis/CoulombRadii/FormDomain/HardyMollifier.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.hardyMollifier line 14
  2. lemma OAI.Coulomb.hardyMollifier_tendsto line 20
  3. lemma OAI.Coulomb.weak_compact_hardy line 25
  4. lemma OAI.Coulomb.ae_nonneg_fatou_integrable_of_bound_tendsto line 77
  5. lemma OAI.Coulomb.realMemLp_bounded_mul line 113
  6. lemma OAI.Coulomb.weak_partial_bounded_mul line 123
  7. lemma OAI.Coulomb.fderiv_smul_input line 159
  8. lemma OAI.Coulomb.exists_hardyCutoffs line 168
  9. lemma OAI.Coulomb.weak_hardy line 229
  10. def OAI.Coulomb.nuclearHardyCoordinates line 298
  11. def OAI.Coulomb.pairHardyCoordinates line 310
  12. lemma OAI.Coulomb.realCLM_mul_ofReal line 325
  13. lemma OAI.Coulomb.weak_complex_component line 330
  14. lemma OAI.Coulomb.complex_norm_sq_components line 350
  15. lemma OAI.Coulomb.complex_weak_hardy line 354
  16. lemma OAI.Coulomb.H1Vector.hardy line 392
  17. def OAI.Coulomb.hardyCoulomb line 400
  18. lemma OAI.Coulomb.hardyCoulomb_nonneg line 403
  19. lemma OAI.Coulomb.hardyCoulomb_sq line 406
  20. lemma OAI.Coulomb.measurable_hardyCoulomb line 410
  21. lemma OAI.Coulomb.quadratic_young_reciprocal line 414
  22. lemma OAI.Coulomb.H1Vector.coulomb_integrable_bound line 422