OAI/Combinatorics/Progressions/Nilpotent/LieBCHContinuity.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.nilpotentSeries line 25
  2. theorem OAI.Erdos3.nilpotentSeries_eq_sum line 28
  3. theorem OAI.Erdos3.nilpotentSeries_eq_finsum line 37
  4. theorem OAI.Erdos3.map_nilpotentSeries line 47
  5. theorem OAI.Erdos3.nilpotentSeries_exp line 53
  6. theorem OAI.Erdos3.hasSubst_C_nilpotent line 63
  7. theorem OAI.Erdos3.subst_C_nilpotent_eq line 68
  8. def OAI.Erdos3.nilpotentSeriesHom line 77
  9. theorem OAI.Erdos3.nilpotentSeriesHom_apply line 81
  10. theorem OAI.Erdos3.nilpotentSeries_X line 86
  11. theorem OAI.Erdos3.isNilpotent_nilpotentSeries line 92
  12. theorem OAI.Erdos3.nilpotentSeries_subst line 99
  13. def OAI.Erdos3.nilpotentLog line 122
  14. theorem OAI.Erdos3.nilpotentLog_eq_sum line 124
  15. theorem OAI.Erdos3.nilpotentLog_zero line 133
  16. theorem OAI.Erdos3.map_nilpotentLog line 136
  17. theorem OAI.Erdos3.isNilpotent_nilpotentLog_comm line 144
  18. theorem OAI.Erdos3.exp_nilpotentLog_comm line 147
  19. theorem OAI.Erdos3.nilpotentLog_exp_sub_one_comm line 154
  20. theorem OAI.Erdos3.isNilpotent_nilpotentLog line 167
  21. theorem OAI.Erdos3.exp_nilpotentLog line 176
  22. theorem OAI.Erdos3.nilpotentLog_exp_sub_one line 187
  23. theorem OAI.Erdos3.exp_injective_on_nilpotents line 198
  24. theorem OAI.Erdos3.nonUnitalSubalgebra_pow_mem line 215
  25. theorem OAI.Erdos3.nilpotentSeries_sub line 225
  26. theorem OAI.Erdos3.nilpotentSeries_one line 229
  27. theorem OAI.Erdos3.nilpotentSeries_mem line 235
  28. theorem OAI.Erdos3.nilpotentLog_mem line 243
  29. theorem OAI.Erdos3.exp_sub_one_mem line 246
  30. theorem OAI.Erdos3.exp_mul_exp_sub_one_mem line 251
  31. def OAI.Erdos3.nilpotentBCH line 262
  32. theorem OAI.Erdos3.nilpotentBCH_mem line 265
  33. theorem OAI.Erdos3.exp_nilpotentBCH line 274
  34. theorem OAI.Erdos3.nilpotentBCH_assoc line 280
  35. theorem OAI.Erdos3.nilpotentBCH_zero_left line 292
  36. theorem OAI.Erdos3.nilpotentBCH_zero_right line 295
  37. theorem OAI.Erdos3.nilpotentBCH_neg_left line 298
  38. theorem OAI.Erdos3.nilpotentBCH_neg_right line 301
  39. theorem OAI.Erdos3.nilpotentBCH_eq_add_of_commute line 304
  40. theorem OAI.Erdos3.nilpotentLog_intertwine line 324
  41. theorem OAI.Erdos3.nilpotentExp_intertwine_injective line 337
  42. theorem OAI.Erdos3.nilpotentExp_bilinear_injective line 351
  43. theorem OAI.Erdos3.nilpotentLog_bilinear line 371
  44. structure OAI.Erdos3.NilpotentBCHGroup line 397
  45. theorem OAI.Erdos3.NilpotentBCHGroup.ext line 406
  46. instance OAI.Erdos3.NilpotentBCHGroup.(instance at line 412) line 412
  47. instance OAI.Erdos3.NilpotentBCHGroup.(instance at line 416) line 416
  48. instance OAI.Erdos3.NilpotentBCHGroup.(instance at line 419) line 419
  49. theorem OAI.Erdos3.NilpotentBCHGroup.coord_mul line 422
  50. theorem OAI.Erdos3.NilpotentBCHGroup.coord_one line 424
  51. theorem OAI.Erdos3.NilpotentBCHGroup.coord_inv line 425
  52. instance OAI.Erdos3.NilpotentBCHGroup.(instance at line 427) line 427
  53. def OAI.Erdos3.NilpotentBCHGroup.expHom line 433
  54. theorem OAI.Erdos3.NilpotentBCHGroup.expHom_val line 444
  55. theorem OAI.Erdos3.NilpotentBCHGroup.expHom_injective line 447
  56. def OAI.Erdos3.NilpotentBCHGroup.unipotentSubgroup line 453
  57. theorem OAI.Erdos3.NilpotentBCHGroup.mem_unipotentSubgroup_iff line 456
  58. def OAI.Erdos3.finiteExp line 482
  59. def OAI.Erdos3.finiteLog line 485
  60. theorem OAI.Erdos3.map_finiteExp line 488
  61. theorem OAI.Erdos3.map_finiteLog line 491
  62. theorem OAI.Erdos3.finiteExp_eq_exp line 494
  63. theorem OAI.Erdos3.finiteLog_eq_log line 497
  64. def OAI.Erdos3.bchPolynomial line 500
  65. def OAI.Erdos3.bchPolynomialEval line 503
  66. theorem OAI.Erdos3.bchPolynomialEval_formula line 506
  67. theorem OAI.Erdos3.bchPolynomialEval_eq line 511
  68. theorem OAI.Erdos3.map_nilpotentBCH line 520
  69. theorem OAI.Erdos3.nilpotentBCH_commuting_maps line 536
  70. structure OAI.Erdos3.NilpotentAlgebraFiltration line 568
  71. def OAI.Erdos3.NilpotentAlgebraFiltration.layerAlgebra line 578
  72. theorem OAI.Erdos3.NilpotentAlgebraFiltration.mem_layerAlgebra line 585
  73. theorem OAI.Erdos3.NilpotentAlgebraFiltration.pow_mem line 588
  74. theorem OAI.Erdos3.NilpotentAlgebraFiltration.pow_eq_zero line 596
  75. theorem OAI.Erdos3.NilpotentAlgebraFiltration.isNilpotent_of_mem line 601
  76. theorem OAI.Erdos3.NilpotentAlgebraFiltration.positive_nilpotent line 604
  77. abbrev OAI.Erdos3.NilpotentAlgebraFiltration.Group line 607
  78. theorem OAI.Erdos3.NilpotentAlgebraFiltration.bchPolynomial_formula line 609
  79. theorem OAI.Erdos3.NilpotentAlgebraFiltration.bch_mem line 613
  80. def OAI.Erdos3.NilpotentAlgebraFiltration.subgroup line 618
  81. theorem OAI.Erdos3.NilpotentAlgebraFiltration.exp_sub_one_mem_layer line 628
  82. theorem OAI.Erdos3.NilpotentAlgebraFiltration.ring_commutator_mem line 632
  83. theorem OAI.Erdos3.NilpotentAlgebraFiltration.mul_mem_right line 637
  84. theorem OAI.Erdos3.NilpotentAlgebraFiltration.exp_commutator_sub_one_mem line 642
  85. theorem OAI.Erdos3.NilpotentAlgebraFiltration.commutator_mem line 662
  86. theorem OAI.Erdos3.NilpotentAlgebraFiltration.subgroup_one line 679
  87. theorem OAI.Erdos3.NilpotentAlgebraFiltration.subgroup_terminal line 684
  88. theorem OAI.Erdos3.NilpotentAlgebraFiltration.descendingCentralSeries line 693
  89. theorem OAI.Erdos3.NilpotentAlgebraFiltration.lowerCentralSeries_eq_bot line 700
  90. theorem OAI.Erdos3.NilpotentAlgebraFiltration.isNilpotentGroup line 706
  91. theorem OAI.Erdos3.NilpotentAlgebraFiltration.nilpotencyClass_le line 709
  92. theorem OAI.Erdos3.seriesMap_commute line 724
  93. theorem OAI.Erdos3.truncatedSeriesMap_commute line 736
  94. def OAI.Erdos3.TruncatedPrimitive line 745
  95. theorem OAI.Erdos3.TruncatedPrimitive.coeff line 750
  96. theorem OAI.Erdos3.truncatedPrimitive_iff_coeff line 757
  97. theorem OAI.Erdos3.TruncatedPrimitive.bch line 765
  98. def OAI.Erdos3.scaledFreeGenerator line 810
  99. theorem OAI.Erdos3.scaledFreeGenerator_positive line 813
  100. theorem OAI.Erdos3.scaledFreeGenerator_primitive line 820
  101. theorem OAI.Erdos3.scaled_bchPolynomial line 830
  102. theorem OAI.Erdos3.bchHomogeneousPart_primitive line 842
  103. theorem OAI.Erdos3.bchHomogeneousPart_mem line 850
  104. theorem OAI.Erdos3.bchTruncation_mem line 854
  105. def OAI.Erdos3.bchLiePolynomial line 861
  106. theorem OAI.Erdos3.bchLiePolynomial_expansion line 864
  107. theorem OAI.Erdos3.bchLiePolynomial_unique line 868
  108. def OAI.Erdos3.lieBCH line 873
  109. def OAI.Erdos3.bchWordCoefficients line 884
  110. def OAI.Erdos3.bchBracketSupport line 887
  111. def OAI.Erdos3.bchBracketCoefficient line 890
  112. theorem OAI.Erdos3.bchWordExpansion_truncation line 893
  113. theorem OAI.Erdos3.bchBracketSupport_length line 900
  114. theorem OAI.Erdos3.lieBCH_bracket_formula line 908
  115. def OAI.Erdos3.bchCoefficientHeight line 915
  116. theorem OAI.Erdos3.bchCoefficientHeight_pos line 919
  117. theorem OAI.Erdos3.bchBracketCoefficient_height line 923
  118. theorem OAI.Erdos3.exists_bch_integer_coefficients line 931
  119. theorem OAI.Erdos3.NilpotentAlgebraFiltration.eval_freeWord_mem line 961
  120. theorem OAI.Erdos3.NilpotentAlgebraFiltration.eval_freeWord_eq_zero line 970
  121. theorem OAI.Erdos3.NilpotentAlgebraFiltration.eval_freeTruncation line 975
  122. theorem OAI.Erdos3.freeLieAssociativeExpansion_eval line 992
  123. theorem OAI.Erdos3.NilpotentAlgebraFiltration.lieBCH_eq line 1000
  124. theorem OAI.Erdos3.continuous_rightBracketList line 1022
  125. theorem OAI.Erdos3.continuous_dynkinWord line 1033
  126. theorem OAI.Erdos3.continuous_lieBCH line 1039
  127. theorem OAI.Erdos3.continuous_lie_of_real_basis line 1056
  128. theorem OAI.Erdos3.continuous_lie_finiteDimensional line 1082