OAI/Geometry/CylinderCovering/Physical/Cost.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderCovering.UnitEdgeFootprints.capPolynomial line 12
  2. def OAI.CylinderCovering.UnitEdgeFootprints.directionPolynomial line 13
  3. def OAI.CylinderCovering.UnitEdgeFootprints.density line 14
  4. def OAI.CylinderCovering.UnitEdgeFootprints.quadraticDensity line 17
  5. lemma OAI.CylinderCovering.UnitEdgeFootprints.polynomial_bounds line 20
  6. lemma OAI.CylinderCovering.UnitEdgeFootprints.local_remainder line 34
  7. lemma OAI.CylinderCovering.UnitEdgeFootprints.density_remainder line 71
  8. lemma OAI.CylinderCovering.UnitEdgeFootprints.sourceCap_sq line 79
  9. lemma OAI.CylinderCovering.UnitEdgeFootprints.density_continuous line 84
  10. lemma OAI.CylinderCovering.UnitEdgeFootprints.quadraticDensity_continuous line 92
  11. lemma OAI.CylinderCovering.UnitEdgeFootprints.quadraticDensity_integral line 96
  12. theorem OAI.CylinderCovering.UnitEdgeFootprints.source_cost_remainder line 115
  13. theorem OAI.CylinderCovering.UnitEdgeFootprints.source_cost_strict line 144
  14. theorem OAI.CylinderCovering.UnitEdgeFootprints.source_cost line 155