OAI/Geometry/Convex/GeneralMahler/IBP.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integration-by-parts formula for the normal measure. Derived by differentiating translations; includes Lipschitz projections.

  1. theorem OAI.GeneralMahler.smoothG_translate_derivative line 13
  2. theorem OAI.GeneralMahler.smoothG_derivative_lipschitz line 33
  3. theorem OAI.GeneralMahler.normal_IBP line 45
  4. theorem OAI.GeneralMahler.normal_IBP_lipschitz line 61