OAI/Geometry/CylinderCovering/Physical/PaddedFinite.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialPhysical.paddedNumerator_continuous line 13
  2. lemma OAI.RadialPhysical.physicalPaddedCap_continuous line 18
  3. lemma OAI.RadialPhysical.paddedNumerator_nonneg line 24
  4. lemma OAI.RadialPhysical.physicalPaddedCap_nonneg line 31
  5. theorem OAI.RadialPhysical.padded_coverage_of_canonical line 38
  6. theorem OAI.RadialPhysical.physicalPadded_cubic_covers line 59
  7. theorem OAI.RadialPhysical.physicalPadded_fractional_covers line 70
  8. theorem OAI.RadialPhysical.padded_finite_of_cover line 82
  9. theorem OAI.RadialPhysical.physicalPadded_cubic_finite line 95
  10. theorem OAI.RadialPhysical.physicalPadded_fractional_finite line 102
  11. theorem OAI.RadialPhysical.eventually_physicalPadded_finite line 109
  12. lemma OAI.RadialPhysical.scaledCost_halve line 122
  13. theorem OAI.RadialPhysical.padded_strict_of_cost line 133
  14. theorem OAI.RadialPhysical.padded_normalized_of_cost line 142
  15. theorem OAI.RadialPhysical.eventually_physicalPadded_strict line 152
  16. theorem OAI.RadialPhysical.physical_padded_finite line 170