OAI/Combinatorics/Progressions/Nilpotent/BCHConjugationLinear.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.lieBCH_eq_of_step_le line 25
  2. theorem OAI.Erdos3.lieBCH_eq_of_nilpotent_steps line 38
  3. theorem OAI.Erdos3.map_lieBCH_of_nilpotent_steps line 44
  4. def OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps line 66
  5. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps_coord line 72
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps_injective line 75
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps_surjective line 80
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapOfSteps_comp line 86
  9. def OAI.Erdos3.NilpotentLieBCHGroup.changeStep line 92
  10. theorem OAI.Erdos3.NilpotentLieBCHGroup.changeStep_coord line 101
  11. theorem OAI.Erdos3.bchSubgroupCoordinates_comap_of_steps line 121
  12. theorem OAI.Erdos3.exists_bchSubgroup_comap_grid_of_steps line 133
  13. def OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate line 169
  14. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_coordinates line 172
  15. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_one line 176
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_comp line 180
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.contDiff_rightTranslate line 187
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_fderiv_leftInverse line 194
  19. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightTranslate_fderiv_injective line 202
  20. def OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity line 209
  21. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_injective line 213
  22. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_one line 218
  23. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightVelocity_mul line 222
  24. theorem OAI.Erdos3.NilpotentLieBCHGroup.contDiff_rightVelocity line 232
  25. def OAI.Erdos3.coordinateDotForm line 263
  26. theorem OAI.Erdos3.coordinateDotForm_apply line 268
  27. theorem OAI.Erdos3.contDiff_bilinearComp_self line 272
  28. def OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm line 296
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_apply line 300
  30. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_symm line 304
  31. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_one line 308
  32. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_pos line 315
  33. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_right_invariant line 328
  34. theorem OAI.Erdos3.NilpotentLieBCHGroup.contDiff_rightInnerForm line 337
  35. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightInnerForm_isVonNBounded line 343
  36. theorem OAI.Erdos3.lieBCH_right_coordinates_sub_bound line 382
  37. theorem OAI.Erdos3.NilpotentLieBCHGroup.lipschitzOn_rightTranslate_box line 435
  38. theorem OAI.Erdos3.NilpotentLieBCHGroup.norm_fderiv_rightTranslate_zero_le line 462
  39. def OAI.Erdos3.NilpotentLieBCHGroup.rightRiemannianMetric line 494
  40. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisChart_mem_source line 515
  41. theorem OAI.Erdos3.NilpotentLieBCHGroup.basis_tangentCoordChange line 523
  42. theorem OAI.Erdos3.NilpotentLieBCHGroup.basis_tangent_trivialization line 537
  43. theorem OAI.Erdos3.NilpotentLieBCHGroup.basis_tangent_symmL line 548
  44. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_rightInnerForm line 559
  45. def OAI.Erdos3.NilpotentLieBCHGroup.rightSmoothRiemannianMetric line 568
  46. theorem OAI.Erdos3.edist_ne_top_of_preconnected line 606
  47. def OAI.Erdos3.NilpotentLieBCHGroup.rightRiemannianBundle line 642
  48. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightRiemannianBundle_continuous line 649
  49. def OAI.Erdos3.NilpotentLieBCHGroup.rightEMetricSpace line 662
  50. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightEMetricSpace_topology line 670
  51. def OAI.Erdos3.NilpotentLieBCHGroup.rightMetricSpace line 675
  52. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightMetricSpace_topology line 679
  53. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightMetricSpace_isRiemannian line 683
  54. theorem OAI.Erdos3.NilpotentLieBCHGroup.basis_extChartAt_apply line 712
  55. theorem OAI.Erdos3.NilpotentLieBCHGroup.basis_extChartAt_symm_apply line 716
  56. theorem OAI.Erdos3.NilpotentLieBCHGroup.mfderiv_mul_right_coordinates line 729
  57. theorem OAI.Erdos3.NilpotentLieBCHGroup.enorm_mfderiv_mul_right line 742
  58. theorem OAI.Erdos3.NilpotentLieBCHGroup.riemannianEDist_mul_right_le line 779
  59. theorem OAI.Erdos3.NilpotentLieBCHGroup.riemannianEDist_mul_right line 789
  60. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightMetricSpace_isometry_mul_right line 798
  61. theorem OAI.Erdos3.NilpotentLieBCHGroup.rightMetricSpace_isIsometricSMul line 807
  62. def OAI.Erdos3.basisCoordinateMap line 823
  63. theorem OAI.Erdos3.basisCoordinateMap_apply line 829
  64. def OAI.Erdos3.realLieHomToRat line 837
  65. def OAI.Erdos3.NilpotentLieBCHGroup.mapReal line 846
  66. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapReal_basisHomeomorph line 858
  67. theorem OAI.Erdos3.NilpotentLieBCHGroup.mapReal_basisHomeomorph_symm line 864
  68. theorem OAI.Erdos3.NilpotentLieBCHGroup.contMDiff_mapReal line 870
  69. theorem OAI.Erdos3.NilpotentLieBCHGroup.mfderiv_mapReal_coordinates line 883
  70. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisCoordinateMap_rightTranslate line 902
  71. def OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates line 932
  72. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_apply line 935
  73. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_rightTranslate line 939
  74. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_continuous line 944
  75. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_zero line 947
  76. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisHomeomorph_pow line 954
  77. theorem OAI.Erdos3.NilpotentLieBCHGroup.basisHomeomorph_zpow line 959
  78. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_nsmul line 964
  79. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_zsmul line 972
  80. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_natCast_smul line 980
  81. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_intCast_smul line 984
  82. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_ratCast_smul line 988
  83. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_smul line 999
  84. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_eq_fderiv line 1009
  85. theorem OAI.Erdos3.NilpotentLieBCHGroup.continuous_conjugation line 1045
  86. theorem OAI.Erdos3.NilpotentLieBCHGroup.contDiff_conjugationCoordinates line 1049
  87. def OAI.Erdos3.NilpotentLieBCHGroup.conjugationLinearMap line 1056
  88. theorem OAI.Erdos3.NilpotentLieBCHGroup.homCoordinates_conjugation_eq line 1059
  89. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationLinearMap_coordinates line 1065
  90. theorem OAI.Erdos3.NilpotentLieBCHGroup.conjugationLinearMap_basis line 1070