OAI/Analysis/PlanarPacking/TableMomentsBase.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Certified quadrature and atomic bounds for the Gaussian moments

  1. def OAI.SharpPlanar.tableMomentRule line 13
  2. def OAI.SharpPlanar.tableMomentIntegral line 15
  3. def OAI.SharpPlanar.tableMomentAtom line 17
  4. def OAI.SharpPlanar.tableMomentK line 21
  5. lemma OAI.SharpPlanar.tableMoment_error line 24
  6. lemma OAI.SharpPlanar.table_kernel_zero_contains line 28
  7. lemma OAI.SharpPlanar.table_kernel_one_contains line 32
  8. def OAI.SharpPlanar.tableAtomBox line 38
  9. lemma OAI.SharpPlanar.tableAtomBox_contains line 40
  10. lemma OAI.SharpPlanar.tableMomentK_contains line 51