OAI/GroupTheory/ArtinCAT0/StableLength.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ArtinCAT0.segment_reverse line 11
  2. lemma OAI.ArtinCAT0.segment_isometry line 21
  3. lemma OAI.ArtinCAT0.comparison_common_start line 28
  4. lemma OAI.ArtinCAT0.segment_unique line 37
  5. lemma OAI.ArtinCAT0.comparison_convexity line 43
  6. lemma OAI.ArtinCAT0.midpoint_comparison line 56
  7. lemma OAI.ArtinCAT0.quadrilateral line 65
  8. def OAI.ArtinCAT0.stableLengthAt line 88
  9. lemma OAI.ArtinCAT0.displacement_subadditive line 91
  10. lemma OAI.ArtinCAT0.stableLength_tendsto line 100
  11. lemma OAI.ArtinCAT0.stableLength_nonneg line 109
  12. lemma OAI.ArtinCAT0.stableLength_le_displacement line 113
  13. lemma OAI.ArtinCAT0.displacement_change_base line 122
  14. lemma OAI.ArtinCAT0.stableLength_basepoint line 129
  15. lemma OAI.ArtinCAT0.stableLength_one line 142
  16. lemma OAI.ArtinCAT0.stableLength_inv line 148
  17. lemma OAI.ArtinCAT0.stableLength_conjugate line 157
  18. lemma OAI.ArtinCAT0.stableLength_pow line 170
  19. lemma OAI.ArtinCAT0.stableLength_mul_le line 185
  20. lemma OAI.ArtinCAT0.displacement_inv line 197
  21. lemma OAI.ArtinCAT0.action_dist line 201
  22. lemma OAI.ArtinCAT0.commuting_displacement_quadrilateral line 205
  23. lemma OAI.ArtinCAT0.length_parallelogram_le line 221
  24. lemma OAI.ArtinCAT0.length_parallelogram line 235
  25. def OAI.ArtinCAT0.lengthPairing line 256
  26. lemma OAI.ArtinCAT0.lengthPairing_symmetric line 259
  27. lemma OAI.ArtinCAT0.lengthPairing_self line 265
  28. lemma OAI.ArtinCAT0.lengthPairing_one line 272
  29. lemma OAI.ArtinCAT0.lengthPairing_polarization line 276
  30. lemma OAI.ArtinCAT0.lengthPairing_inv line 284
  31. lemma OAI.ArtinCAT0.lengthPairing_conjugate line 292
  32. lemma OAI.ArtinCAT0.lengthPairing_jensen line 298
  33. lemma OAI.ArtinCAT0.lengthPairing_mul_left line 316
  34. lemma OAI.ArtinCAT0.lengthPairing_mul_right line 330
  35. lemma OAI.ArtinCAT0.lengthPairing_pow_right line 338
  36. lemma OAI.ArtinCAT0.lengthPairing_pow_left line 349
  37. lemma OAI.ArtinCAT0.stableLength_product_sq line 356
  38. lemma OAI.ArtinCAT0.stableLength_zpow line 362
  39. lemma OAI.ArtinCAT0.lengthPairing_zpow_right line 371
  40. lemma OAI.ArtinCAT0.finite_movers_of_compact line 388
  41. lemma OAI.ArtinCAT0.exists_displacement_minimizer line 406
  42. lemma OAI.ArtinCAT0.segment_point_eq_of_dist line 448
  43. lemma OAI.ArtinCAT0.minimizer_displacement_two line 462
  44. lemma OAI.ArtinCAT0.powerStepDistance line 477
  45. lemma OAI.ArtinCAT0.extension_numeric line 482
  46. lemma OAI.ArtinCAT0.minimizer_displacement_pow line 495
  47. lemma OAI.ArtinCAT0.stableLength_minimizer line 548
  48. lemma OAI.ArtinCAT0.lengthPairing_basepoint line 558
  49. lemma OAI.ArtinCAT0.stableLength_finiteOrder line 562
  50. lemma OAI.ArtinCAT0.finiteOrder_of_fixedPoint line 569
  51. lemma OAI.ArtinCAT0.stableLength_eq_zero_iff_finiteOrder line 583
  52. lemma OAI.ArtinCAT0.lengthPairing_zpow_left line 591
  53. lemma OAI.ArtinCAT0.stableLength_zpow_product_sq line 598
  54. lemma OAI.ArtinCAT0.nonpos_of_nat_mul_le line 608
  55. lemma OAI.ArtinCAT0.zero_of_int_mul_le line 613
  56. lemma OAI.ArtinCAT0.lengthPairing_zero_of_length_zero line 621