OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateIntegrationByParts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts for the pure coordinate derivatives, with compact positive-height tests and no assumption on mixed derivatives.

  1. lemma OAI.CubicFirstMoment.cubicThetaAxisFirst_continuousOn line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaCoordinate_integrationByParts line 27