OAI/Geometry/Cannon/Beltrami/Mollifier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonBeltrami.mollifier line 62
  2. def OAI.CannonBeltrami.mollify line 68
  3. lemma OAI.CannonBeltrami.locallyIntegrable_bounded line 71
  4. lemma OAI.CannonBeltrami.mollify_smooth line 77
  5. lemma OAI.CannonBeltrami.mollify_bound line 82
  6. lemma OAI.CannonBeltrami.mollify_zero line 90
  7. lemma OAI.CannonBeltrami.mollify_compact line 107
  8. lemma OAI.CannonBeltrami.mollify_ae_tendsto line 117
  9. theorem OAI.CannonBeltrami.exists_smooth_coefficient_approximation line 124
  10. def OAI.CannonBeltrami.globalCutoff line 141
  11. theorem OAI.CannonBeltrami.global_smooth_coefficient_approximation line 147
  12. theorem OAI.CannonBeltrami.global_weak_mrmt line 185