OAI/Geometry/Convex/GeneralMahler/ProjParts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gaussian parts with an affine test; used to make moment continuity independent of pointwise convergence of projection derivatives.

  1. lemma OAI.GeneralMahler.ProjField.weighted_P_integrable line 17
  2. theorem OAI.GeneralMahler.ProjField.weighted_P_ip line 26