OAI/Analysis/CoulombRadii/FormDomain/WeakSchwartzDerivative.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.compact_mul_memLp_integrable line 18
  2. lemma OAI.Coulomb.compact_complex_integral_decompose line 22
  3. lemma OAI.Coulomb.weak_directional_complex_test line 39
  4. def OAI.Coulomb.weakCutBump line 63
  5. def OAI.Coulomb.weakCut line 64
  6. lemma OAI.Coulomb.weakCut_smooth line 65
  7. lemma OAI.Coulomb.weakCut_compact line 67
  8. lemma OAI.Coulomb.weakCut_fderiv line 70
  9. lemma OAI.Coulomb.weakCut_bound line 77
  10. lemma OAI.Coulomb.weakCut_tendsto line 88
  11. lemma OAI.Coulomb.weak_directional_schwartz_test line 100
  12. lemma OAI.Coulomb.l2_weakDeriv_tempered line 185