OAI/Geometry/CylinderCovering/Radial/PairedSweep.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.RadialPairedSweep.point_inner line 12
  2. lemma OAI.CylinderCovering.RadialPairedSweep.point_norm_sq line 16
  3. lemma OAI.CylinderCovering.RadialPairedSweep.point_x_unit line 20
  4. lemma OAI.CylinderCovering.RadialPairedSweep.point_y_unit line 24
  5. lemma OAI.CylinderCovering.RadialPairedSweep.upper_independent line 28
  6. lemma OAI.CylinderCovering.RadialPairedSweep.lower_independent line 39
  7. lemma OAI.CylinderCovering.RadialPairedSweep.G_deriv line 50
  8. def OAI.CylinderCovering.RadialPairedSweep.upperW line 55
  9. def OAI.CylinderCovering.RadialPairedSweep.lowerW line 58
  10. lemma OAI.CylinderCovering.RadialPairedSweep.upperW_deriv line 61
  11. lemma OAI.CylinderCovering.RadialPairedSweep.lowerW_deriv line 77
  12. def OAI.CylinderCovering.RadialPairedSweep.upperData line 93
  13. def OAI.CylinderCovering.RadialPairedSweep.lowerData line 123
  14. lemma OAI.CylinderCovering.RadialPairedSweep.upperW_eq line 153
  15. lemma OAI.CylinderCovering.RadialPairedSweep.lowerW_eq line 158
  16. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_sweep line 167
  17. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_sweep line 181
  18. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_direction line 195
  19. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_direction line 204
  20. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_kappa line 213
  21. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_kappa line 221
  22. lemma OAI.CylinderCovering.RadialPairedSweep.upperW_norm_sq line 229
  23. lemma OAI.CylinderCovering.RadialPairedSweep.lowerW_norm_sq line 234
  24. lemma OAI.CylinderCovering.RadialPairedSweep.upperData_weightedArea line 239
  25. lemma OAI.CylinderCovering.RadialPairedSweep.lowerData_weightedArea line 249
  26. theorem OAI.CylinderCovering.RadialPairedSweep.paired_radial_sweeps line 259
  27. lemma OAI.CylinderCovering.RadialPairedSweep.physicalCost_sqrt_two line 280
  28. theorem OAI.CylinderCovering.RadialPairedSweep.exists_pair_below line 288