OAI/Geometry/CylinderCovering/Nilpotent/RateCost.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.NilpotentRate.center_tag_distance line 12
  2. theorem OAI.CylinderCovering.NilpotentRate.fine_center_weight_error line 24
  3. theorem OAI.CylinderCovering.NilpotentRate.fine_weighted_cell_bound line 43
  4. def OAI.CylinderCovering.NilpotentRate.secondFiber line 85
  5. theorem OAI.CylinderCovering.NilpotentRate.sum_pairs_eq_fibers line 88
  6. theorem OAI.CylinderCovering.NilpotentRate.mem_secondFiber line 103
  7. theorem OAI.CylinderCovering.NilpotentRate.constructionCost_eq_sum line 117
  8. def OAI.CylinderCovering.NilpotentRate.localCostError line 138
  9. theorem OAI.CylinderCovering.NilpotentRate.localCostError_nonneg line 144
  10. theorem OAI.CylinderCovering.NilpotentRate.constructionCost_le_tagged_sum line 149