OAI/Analysis/BoxTransport/Geometry.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Quantitative box separation, affine images and positive diagonal shape estimates.

  1. theorem OAI.BoxTransport.Routing.mixedDerivative_zero line 13
  2. theorem OAI.BoxTransport.Routing.effective_zero line 19
  3. theorem OAI.BoxTransport.Routing.admissible_zero line 29
  4. theorem OAI.BoxTransport.Routing.globalFlow_zero line 37
  5. theorem OAI.BoxTransport.Routing.identity_routing line 46
  6. theorem OAI.BoxTransport.Routing.empty_routing line 57
  7. theorem OAI.BoxTransport.Routing.center_mem_realBox line 63
  8. theorem OAI.BoxTransport.Routing.realBox_disjoint_of_gap line 67
  9. theorem OAI.BoxTransport.Routing.realBox_disjoint_iff line 80
  10. theorem OAI.BoxTransport.Routing.solidBox_disjoint_iff line 115
  11. theorem OAI.BoxTransport.Routing.centers_ne_of_disjoint line 138
  12. theorem OAI.BoxTransport.Routing.expansion_preserves_disjoint line 145
  13. theorem OAI.BoxTransport.Routing.padded_boxes_disjoint_of_clearance line 157
  14. def OAI.BoxTransport.Routing.coordinateGap line 170
  15. theorem OAI.BoxTransport.Routing.coordinateGap_pos_iff line 174
  16. theorem OAI.BoxTransport.Routing.positive_finset_lower_bound line 179
  17. theorem OAI.BoxTransport.Routing.uniform_rational_gap line 195
  18. theorem OAI.BoxTransport.Routing.exists_expansion_factor line 214
  19. theorem OAI.BoxTransport.Routing.exists_rational_padding line 260
  20. def OAI.BoxTransport.Routing.parkingCenter line 302
  21. theorem OAI.BoxTransport.Routing.parking_separated line 305
  22. theorem OAI.BoxTransport.Routing.parking_clearance line 317
  23. theorem OAI.BoxTransport.Routing.exists_parking_offset line 326
  24. theorem OAI.BoxTransport.Routing.smooth_power_scale line 337
  25. theorem OAI.BoxTransport.Routing.power_scale_between line 342
  26. theorem OAI.BoxTransport.Routing.determinant_power_scale line 354
  27. theorem OAI.BoxTransport.Routing.geometric_halfwidth_le line 360
  28. theorem OAI.BoxTransport.Routing.reshaping_properties line 378
  29. theorem OAI.BoxTransport.Routing.diagonal_affine_image line 391
  30. theorem OAI.BoxTransport.Routing.prescribedAffine_image line 416
  31. def OAI.BoxTransport.Routing.openBox line 432
  32. theorem OAI.BoxTransport.Routing.isOpen_openBox line 435
  33. theorem OAI.BoxTransport.Routing.realBox_subset_openBox line 443
  34. theorem OAI.BoxTransport.Routing.affine_openBox_control line 448