OAI/Geometry/CylinderCovering/Nilpotent/Construction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Nilpotent.quadratic_inversion_nonneg line 9
  2. theorem OAI.CylinderCovering.Nilpotent.quadratic_inversion line 42
  3. theorem OAI.CylinderCovering.Nilpotent.v_bounds line 52
  4. theorem OAI.CylinderCovering.Nilpotent.a_bounds line 57
  5. theorem OAI.CylinderCovering.Nilpotent.height_gt_half line 65
  6. theorem OAI.CylinderCovering.Nilpotent.overlap_pair_inequality line 72
  7. theorem OAI.CylinderCovering.Nilpotent.overlap_identity line 77
  8. theorem OAI.CylinderCovering.Nilpotent.center_error line 86
  9. theorem OAI.CylinderCovering.Nilpotent.abs_product_le_one line 99
  10. theorem OAI.CylinderCovering.Nilpotent.coefficient_pos line 104
  11. theorem OAI.CylinderCovering.Nilpotent.cutoff_mix_lower line 114
  12. theorem OAI.CylinderCovering.Nilpotent.failed_cutoffs_lower line 128
  13. theorem OAI.CylinderCovering.Nilpotent.centered_product_upper line 146
  14. theorem OAI.CylinderCovering.Nilpotent.centered_overlap_upper line 159
  15. theorem OAI.CylinderCovering.Nilpotent.cutoff_alternative line 174
  16. theorem OAI.CylinderCovering.Nilpotent.sweep_cover line 212