OAI/Combinatorics/Progressions/Nilpotent/BCHNonlinearRemainder.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.map_freeLie_lift line 11
  2. theorem OAI.Erdos3.map_lieBCH line 19
  3. def OAI.Erdos3.scaledFreeLieEval line 28
  4. theorem OAI.Erdos3.scaledFreeLieEval_of line 32
  5. theorem OAI.Erdos3.scaledFreeLieEval_eq line 36
  6. theorem OAI.Erdos3.lie_lift_eq_of_scaledFreeLieEval_eq line 47
  7. theorem OAI.Erdos3.scaledFreeGenerator_mem_layer line 64
  8. theorem OAI.Erdos3.lieBCH_assoc line 68
  9. theorem OAI.Erdos3.lieBCH_zero_left line 84
  10. theorem OAI.Erdos3.lieBCH_neg_left line 96
  11. structure OAI.Erdos3.NilpotentLieBCHGroup line 108
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.ext line 115
  13. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 121) line 121
  14. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 124) line 124
  15. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 127) line 127
  16. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_mul line 130
  17. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_one line 132
  18. theorem OAI.Erdos3.NilpotentLieBCHGroup.coord_inv line 133
  19. instance OAI.Erdos3.NilpotentLieBCHGroup.(instance at line 135) line 135
  20. def OAI.Erdos3.NilpotentLieBCHGroup.map line 141
  21. def OAI.Erdos3.lieBCHList line 159
  22. theorem OAI.Erdos3.map_lieBCHList line 163
  23. theorem OAI.Erdos3.lieBCHList_group_prod line 169
  24. def OAI.Erdos3.bchProductLiePolynomial line 178
  25. theorem OAI.Erdos3.bchProductLiePolynomial_eval line 181
  26. theorem OAI.Erdos3.bchProductLiePolynomial_support_length line 189
  27. theorem OAI.Erdos3.lieBCH_mem line 202
  28. def OAI.Erdos3.NilpotentLieBCHGroup.subgroup line 212
  29. theorem OAI.Erdos3.NilpotentLieBCHGroup.mem_subgroup line 218
  30. def OAI.Erdos3.lieQuotientMap line 223
  31. theorem OAI.Erdos3.lieQuotientMap_surjective line 226
  32. theorem OAI.Erdos3.lieQuotientMap_eq_zero line 229
  33. theorem OAI.Erdos3.lie_quotient_lowerCentralSeries_eq_bot line 232
  34. def OAI.Erdos3.bchProductPolynomial line 249
  35. theorem OAI.Erdos3.bchProductPolynomial_eval line 253
  36. theorem OAI.Erdos3.NilpotentAlgebraFiltration.lieBCHList_mem line 263
  37. theorem OAI.Erdos3.NilpotentAlgebraFiltration.exp_lieBCHList line 271
  38. theorem OAI.Erdos3.NilpotentAlgebraFiltration.bchProductPolynomial_formula line 280
  39. theorem OAI.Erdos3.bchProductLiePolynomial_associativeExpansion line 297
  40. def OAI.Erdos3.NilpotentAlgebraFiltration.extend line 329
  41. theorem OAI.Erdos3.lieBCH_eq_add_of_isLieAbelian line 343
  42. theorem OAI.Erdos3.lieBCH_eq_add_of_lie_eq_zero_pos line 365
  43. theorem OAI.Erdos3.lieBCH_eq_add_of_lie_eq_zero line 384
  44. def OAI.Erdos3.bchBoxCoordinateBound line 406
  45. theorem OAI.Erdos3.bchBoxCoordinateBound_nonneg line 410
  46. theorem OAI.Erdos3.lieBCH_sub_coordinates_bound line 415
  47. def OAI.Erdos3.bchProductWordCoefficients line 477
  48. def OAI.Erdos3.bchProductBracketSupport line 480
  49. def OAI.Erdos3.bchProductBracketCoefficient line 483
  50. theorem OAI.Erdos3.bchProductBracketSupport_length line 486
  51. theorem OAI.Erdos3.bchProductWordCoefficients_eq line 490
  52. theorem OAI.Erdos3.lieBCHList_bracket_formula line 497
  53. def OAI.Erdos3.bchProductCoordinatePolynomial line 509
  54. theorem OAI.Erdos3.bchProductCoordinatePolynomial_totalDegree line 514
  55. theorem OAI.Erdos3.bchProductCoordinatePolynomial_support_card line 524
  56. theorem OAI.Erdos3.bchProductCoordinatePolynomial_eval line 531
  57. theorem OAI.Erdos3.bchProductCoordinatePolynomial_eval_over line 542
  58. theorem OAI.Erdos3.lieBCH_sub_right_mem_of_mem_ideal line 566
  59. theorem OAI.Erdos3.lieBCH_sub_left_mem_of_mem_ideal line 573
  60. theorem OAI.Erdos3.dynkinWord_eq_zero_of_abelian line 591
  61. theorem OAI.Erdos3.bch_linear_words_sum line 600
  62. theorem OAI.Erdos3.lieBCH_eq_add_nonlinear_sum line 626