OAI/Geometry/CylinderCovering/Nilpotent/SmoothRate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.NilpotentRate.cell_cover line 12
  2. theorem OAI.CylinderCovering.NilpotentRate.choose_tags_frames line 18
  3. theorem OAI.CylinderCovering.NilpotentRate.sliding_rows_of_frame line 41
  4. theorem OAI.CylinderCovering.NilpotentRate.nilpotent_inverse_norm_bound line 85
  5. theorem OAI.CylinderCovering.NilpotentRate.selected_center_near_cell line 108
  6. theorem OAI.CylinderCovering.NilpotentRate.construction_covers_of_bounds line 136