OAI/Geometry/Convex/GeneralMahler/Smoothing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Gaussian smoothing and an integration by parts formula.

  1. theorem OAI.GeneralMahler.hasDeriv_nDensity_shift line 11
  2. theorem OAI.GeneralMahler.nDensity_shift_bound line 20
  3. def OAI.GeneralMahler.smoothG line 34
  4. lemma OAI.GeneralMahler.smoothG_eq line 36
  5. abbrev OAI.GeneralMahler.G' line 42
  6. lemma OAI.GeneralMahler.continuous_pair_G' line 45
  7. theorem OAI.GeneralMahler.smooth_domination line 52
  8. theorem OAI.GeneralMahler.strongly_G' line 79
  9. theorem OAI.GeneralMahler.smoothG_hasFDeriv line 93
  10. theorem OAI.GeneralMahler.continuous_smoothG line 119
  11. theorem OAI.GeneralMahler.smoothG_deriv_cont line 123