OAI/Analysis/PlanarPacking/HighMomentsBase.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Interval enclosures for direct and transformed moments of arbitrary order

  1. def OAI.SharpPlanar.fullFactor line 9
  2. def OAI.SharpPlanar.fullMomentRule line 11
  3. def OAI.SharpPlanar.fullMomentIntegral line 13
  4. def OAI.SharpPlanar.fullMomentAtom line 15
  5. def OAI.SharpPlanar.fullMoment line 18
  6. lemma OAI.SharpPlanar.fullMoment_error line 20
  7. lemma OAI.SharpPlanar.fullAtomBox_contains line 25
  8. lemma OAI.SharpPlanar.fullMoment_contains line 34
  9. lemma OAI.SharpPlanar.fullFactor_step_contains line 43