OAI/Analysis/CircleDomains/Selection/VerticalCylinderCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A narrow vertical cylinder has a finite small-diameter cover whose quadratic cost is controlled by its height times its base radius.

  1. lemma OAI.CircleDomainRigidity.vertical_cylinder_cover line 13