OAI/Analysis/CoulombRadii/Propagation/MaximumMollifier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.maximumBump line 14
  2. def OAI.NeutralAtom.maximumMollify line 19
  3. lemma OAI.NeutralAtom.maximumBump_rOut_le_one line 22
  4. lemma OAI.NeutralAtom.maximumBump_rOut_tendsto line 26
  5. lemma OAI.NeutralAtom.maximumMollify_contDiff line 29
  6. lemma OAI.NeutralAtom.maximumMollify_tendsto line 34
  7. lemma OAI.NeutralAtom.maximumMollify_ae_tendsto line 40
  8. lemma OAI.NeutralAtom.weakLaplacianGE_maximumMollify line 46
  9. lemma OAI.NeutralAtom.maximumMollify_abs_le line 60
  10. lemma OAI.NeutralAtom.maximumMollify_abs_le_ball line 82
  11. lemma OAI.NeutralAtom.continuous_softWeight line 98
  12. lemma OAI.NeutralAtom.convex_pair_abs_le line 102
  13. lemma OAI.NeutralAtom.tendsto_integral_compact_mul line 113
  14. lemma OAI.NeutralAtom.weakLaplacianGE_maximumMollify_local line 131
  15. theorem OAI.NeutralAtom.WeakLaplacianGE.max_tied line 146