OAI/GroupTheory/ArtinCAT0/Pairing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArtinCAT0.orbitBusemann line 14

    Source documentation

    Busemann function based on the positive orbit of a minimizing point.

    noncomputable def orbitBusemann (x : X) (g : G) (D : ℝ) (z : X) : ℝ :=
…
  2. lemma OAI.ArtinCAT0.orbitBusemann_tendsto line 17
  3. lemma OAI.ArtinCAT0.orbitBusemann_lipschitz line 36
  4. lemma OAI.ArtinCAT0.fourSquares_limit line 44
  5. lemma OAI.ArtinCAT0.quadrilateral_difference line 61
  6. lemma OAI.ArtinCAT0.orbitBusemann_centralizer_difference line 71
  7. def OAI.ArtinCAT0.orbitCharacter line 107
  8. lemma OAI.ArtinCAT0.orbitCharacter_one line 110
  9. lemma OAI.ArtinCAT0.orbitCharacter_mul line 113
  10. lemma OAI.ArtinCAT0.orbitCharacter_pow line 124
  11. lemma OAI.ArtinCAT0.orbitCharacter_inv line 137
  12. lemma OAI.ArtinCAT0.orbitCharacter_zpow line 147
  13. lemma OAI.ArtinCAT0.orbitBusemann_self line 161
  14. lemma OAI.ArtinCAT0.orbitCharacter_self line 168
  15. lemma OAI.ArtinCAT0.orbitCharacter_abs_le line 183
  16. lemma OAI.ArtinCAT0.lengthPairing_eq_orbitCharacter line 196
  17. lemma OAI.ArtinCAT0.lengthPairing_centralizer line 217