OAI/Combinatorics/Progressions/Nilpotent/BCHLatticeImageGap.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_mapReal line 24
  2. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_tangent_eq_coordinateL2Norm line 60
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_mfderiv_mapReal_le line 84
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_mapReal_of_coordinate_bound line 112
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_changeStep line 147
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.isometry_changeStep line 157
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_fderiv_zero_rightVelocity line 188
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.coordinate_norm_le_rightVelocity line 197
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.mfderiv_basisHomeomorph_coordinates line 215
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_mfderiv_basisHomeomorph_le line 230
  11. def OAI.Erdos3.NilpotentLieBCHGroup.coordinateLine line 267
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.coordinateLine_zero line 272
  13. theorem OAI.Erdos3.NilpotentLieBCHGroup.coordinateLine_one line 277
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_coordinateLine line 281
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_coordinateLine_inv line 287
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_coordinateLine line 295
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.mfderiv_coordinateLine line 310
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.linear_hom_basisHomeomorph line 351
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_linear_hom line 355
  20. theorem OAI.Erdos3.NilpotentLieBCHGroup.mfderiv_linear_hom_coordinates line 367
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_linear_hom line 384
  22. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_mfderiv_linear_hom_le line 400
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitz_linear_hom line 425
  24. def OAI.Erdos3.bchLogMetricConstant line 452
  25. theorem OAI.Erdos3.bchLogMetricConstant_pos line 456
  26. theorem OAI.Erdos3.NilpotentLieBCHGroup.edist_coordinates_le_of_near_one line 471
  27. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_coordinates_le_of_near_one line 502
  28. def OAI.Erdos3.bchInverseBoxConstant line 536
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_coordinates_le_bchInverseBoxConstant line 549
  30. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitzOn_basisHomeomorph_box line 605
  31. def OAI.Erdos3.bchLatticeSeparationRadius line 626
  32. theorem OAI.Erdos3.bchLatticeSeparationRadius_pos line 629
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.eq_one_of_subgroup_of_dist_lt line 643
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.latticeSeparationRadius_le_dist line 668
  35. theorem OAI.Erdos3.one_le_bchLogMetricConstant line 691
  36. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_coordinates_le_of_near_box line 705
  37. theorem OAI.Erdos3.NilpotentLieBCHGroup.dist_coordinates_le_of_near_unit_box line 747
  38. theorem OAI.Erdos3.NilpotentLieBCHGroup.rational_kernel_of_near_bounded_point line 805
  39. theorem OAI.Erdos3.NilpotentLieBCHGroup.lattice_translate_mem_of_small_dist line 852
  40. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_lattice_image_gap line 890