OAI/Combinatorics/Progressions/Nilpotent/BCHQuotientLocalIsometry.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_compact_realification_representatives line 27
  2. theorem OAI.Erdos3.compactSpace_realification_quotient line 50
  3. theorem OAI.Erdos3.exists_realification_cocompact_lattice line 59
  4. theorem OAI.Erdos3.isCoveringMap_realification_quotient line 101
  5. theorem OAI.Erdos3.exists_realification_lieGroup_lattice line 111
  6. def OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace line 156
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_topology line 165
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_edist_mk line 171
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotientMetricSpace_lipschitz_mk line 179
  10. def OAI.Erdos3.realificationQuotientMetricSpace line 205
  11. theorem OAI.Erdos3.realificationQuotientMetricSpace_topology line 213
  12. theorem OAI.Erdos3.realificationQuotientMetricSpace_compact line 219
  13. def OAI.Erdos3.realificationLieHom line 240
  14. theorem OAI.Erdos3.realificationLieHom_tmul line 245
  15. theorem OAI.Erdos3.realificationLieHom_inclusion line 248
  16. theorem OAI.Erdos3.realificationLieHom_basis line 251
  17. def OAI.Erdos3.NilpotentLieBCHGroup.realificationMap line 263
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_coord line 268
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_realificationHom_ofSteps line 272
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_realificationHom line 279
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_subgroup line 287
  22. def OAI.Erdos3.coordinateLipschitzBound line 309
  23. theorem OAI.Erdos3.coordinateLipschitzBound_pos line 312
  24. theorem OAI.Erdos3.coordinateLipschitzBound_le_exp line 317
  25. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_mapReal_of_entry_bound line 351
  26. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_mapReal_of_rational_height line 361
  27. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_mapReal_lipschitz_exp_bound line 373
  28. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_quotient_mapReal_of_entry_bound line 390
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_quotient_mapReal_lipschitz_exp_bound line 405
  30. def OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist line 436
  31. def OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist line 440
  32. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist_mapReal_le line 458
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist_mapReal_le line 467
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapReal_id line 490
  35. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist_change_le line 493
  36. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist_compare line 500
  37. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist_exp_change_le line 509
  38. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisRiemannianDist_exp_compare line 520
  39. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist_change_le line 531
  40. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist_compare line 547
  41. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist_exp_change_le line 559
  42. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisQuotientDist_exp_compare line 571
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_conjugation_of_basis_bound line 603
  44. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_mul_left_of_basis_bound line 617
  45. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_realificationMap line 649
  46. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_realificationMap_lipschitz_exp_bound line 658
  47. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_realificationMap_quotient line 672
  48. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_realificationMap_quotient_lipschitz_exp_bound line 691
  49. theorem OAI.Erdos3.NilpotentLieBCHGroup.quotient_dist_eq_on_ball_of_lattice_grid line 723