OAI/Analysis/HenonEmden/Mollification.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.WeakPDE.convolve line 28
  2. lemma OAI.HenonLaneEmden.WeakPDE.convolve_def line 30
  3. lemma OAI.HenonLaneEmden.WeakPDE.contDiff_convolve line 32
  4. lemma OAI.HenonLaneEmden.WeakPDE.dir_convolve line 36
  5. lemma OAI.HenonLaneEmden.WeakPDE.laplacian_convolve line 44
  6. lemma OAI.HenonLaneEmden.WeakPDE.laplacian_translate line 67
  7. lemma OAI.HenonLaneEmden.WeakPDE.laplacian_reflect line 73
  8. lemma OAI.HenonLaneEmden.WeakPDE.convolve_nonneg line 86
  9. lemma OAI.HenonLaneEmden.WeakPDE.convolve_comm line 89
  10. lemma OAI.HenonLaneEmden.WeakPDE.convolve_weak_equation line 96
  11. lemma OAI.HenonLaneEmden.WeakPDE.convolve_normed_tendsto line 108
  12. lemma OAI.HenonLaneEmden.WeakPDE.smooth_newton_lower line 125
  13. def OAI.HenonLaneEmden.WeakPDE.standardBump line 141
  14. lemma OAI.HenonLaneEmden.WeakPDE.standardBump_tendsto line 147
  15. lemma OAI.HenonLaneEmden.WeakPDE.weak_newton_lower line 151