OAI/Geometry/ConjugatePoints/Convexity.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Midpoint convexity, minsets, and the semisimple shear obstruction.

  1. structure OAI.ThreeManifold.NonpositiveMetric.CNMidpoint line 16
  2. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_dist_left line 24
  3. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_dist_right line 32
  4. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.eq_mid_of_dist_le line 40
  5. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_comm line 46
  6. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_self line 50
  7. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_isometry line 54
  8. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_common line 60
  9. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.mid_convex line 67
  10. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimum_step_two line 74
  11. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimum_midpoint line 84
  12. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.MidConvex line 103
  13. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.halfSequence line 105
  14. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.halfSequence_mem line 111
  15. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.halfSequence_dist line 117
  16. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.halfSequence_CN line 125
  17. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.projection_angle line 137
  18. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.quadrilateral line 154
  19. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.projection_nonexpansive line 168
  20. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.projection_unique line 179
  21. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.isometry_iterate line 189
  22. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimum_iterate_displacement line 195
  23. theorem OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimizing_orbit_linear line 201
  24. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minset line 244
  25. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minset_closed line 246
  26. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minset_midConvex line 253
  27. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minset_map line 261
  28. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minset_preimage line 267
  29. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.exists_projection line 274
  30. theorem OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.commuting_common_minimum line 284
  31. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.line_midpoint line 304
  32. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.line_midConvex line 315
  33. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.exists_line_coordinate line 320
  34. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate line 327
  35. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate_min line 331
  36. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate_unique line 335
  37. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate_nonexpansive line 342
  38. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate_shift line 349
  39. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.nonexpansive_of_period line 361
  40. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.parallel_line_coordinate line 387
  41. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.bounded_midpoint_convex_constant line 400
  42. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.parallel_line_separation line 419
  43. theorem OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.parallel_line_distance line 441
  44. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift line 479
  45. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.lineCoordinate_self line 483
  46. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.centralizer_line_distance line 490
  47. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.linear_bounded_zero line 505
  48. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift_mul line 512
  49. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift_one line 535
  50. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift_self line 538
  51. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift_inv line 543
  52. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisShift_commutator line 550
  53. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.equiv_pow_iterate line 565
  54. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimizing_zpow_dist line 571
  55. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.minimizing_zpow_dist_pair line 585
  56. def OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin line 595
  57. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin_shift line 598
  58. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin_zero line 606
  59. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin_start_dist line 610
  60. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin_end_dist line 617
  61. lemma OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.axisJoin_dist line 624
  62. theorem OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.exists_minimizing_axis line 668
  63. theorem OAI.ThreeManifold.NonpositiveMetric.CNMidpoint.cyclic_shear_obstruction line 696