OAI/Geometry/CylinderCovering/Footprints/Footprints.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Footprints.quadraticIntercept_transverse line 9
  2. theorem OAI.CylinderCovering.Footprints.radial_displacement_bound line 15
  3. theorem OAI.CylinderCovering.Footprints.transverse_displacement_bound line 25
  4. theorem OAI.CylinderCovering.Footprints.quadratic_mem_absolute line 39
  5. theorem OAI.CylinderCovering.Footprints.quadratic_mem_absolute_midpoint line 61
  6. theorem OAI.CylinderCovering.Footprints.quadratic_mem_affine_midpoint line 85
  7. theorem OAI.CylinderCovering.Footprints.quadratic_mem_endpoint line 116
  8. theorem OAI.CylinderCovering.Footprints.integral_affine_width line 142
  9. theorem OAI.CylinderCovering.Footprints.integral_absolute_width line 152
  10. theorem OAI.CylinderCovering.Footprints.volume_closedBand_eq_integral line 187
  11. theorem OAI.CylinderCovering.Footprints.volume_absoluteFootprint line 215
  12. theorem OAI.CylinderCovering.Footprints.affine_width_nonneg line 247
  13. theorem OAI.CylinderCovering.Footprints.volume_affineFootprint line 254
  14. theorem OAI.CylinderCovering.Footprints.endpointFootprint_eq_affine line 286
  15. theorem OAI.CylinderCovering.Footprints.volume_endpointFootprint line 296
  16. theorem OAI.CylinderCovering.Footprints.absoluteArea_nonneg line 303
  17. theorem OAI.CylinderCovering.Footprints.affineArea_nonneg line 307
  18. theorem OAI.CylinderCovering.Footprints.realVolume_absoluteFootprint line 311
  19. theorem OAI.CylinderCovering.Footprints.realVolume_affineFootprint line 318
  20. theorem OAI.CylinderCovering.Footprints.isCompact_closedBand line 325
  21. theorem OAI.CylinderCovering.Footprints.isCompact_absoluteFootprint line 341
  22. theorem OAI.CylinderCovering.Footprints.isCompact_affineFootprint line 360
  23. theorem OAI.CylinderCovering.Footprints.isCompact_endpointFootprint line 379
  24. theorem OAI.CylinderCovering.Footprints.convex_affineFootprint line 384
  25. theorem OAI.CylinderCovering.Footprints.not_convex_absoluteFootprint line 402
  26. theorem OAI.CylinderCovering.Footprints.absoluteArea_error_bound line 437
  27. theorem OAI.CylinderCovering.Footprints.affineArea_error_bound line 454
  28. theorem OAI.CylinderCovering.Footprints.sum_absoluteArea_error_bound line 471
  29. theorem OAI.CylinderCovering.Footprints.midpoint_table_containment line 492
  30. theorem OAI.CylinderCovering.Footprints.generous_absolute_containment line 506
  31. theorem OAI.CylinderCovering.Footprints.midpoint_affine_subset_absolute line 516
  32. theorem OAI.CylinderCovering.Footprints.midpoint_area_difference line 525
  33. theorem OAI.CylinderCovering.Footprints.midpoint_affineArea_lt_absoluteArea line 531
  34. theorem OAI.CylinderCovering.Footprints.physical_quadratic_intercept line 539