OAI/Combinatorics/Progressions/Estimates/FreeLieTreeCoefficientBounds.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.wordPolynomialEmbedding_single line 13
  2. theorem OAI.Erdos3.freeSemigroup_toFreeMonoid_length line 19
  3. theorem OAI.Erdos3.wordPolynomialEmbedding_truncation line 25
  4. theorem OAI.Erdos3.wordPolynomialEmbedding_freeLieExpansion line 35
  5. theorem OAI.Erdos3.lie_lift_eq_of_freeTruncation_eq line 39
  6. theorem OAI.Erdos3.freeTruncation_eq_of_scaled_series_eq line 51
  7. theorem OAI.Erdos3.lie_lift_eq_of_scaled_series_eq line 59
  8. def OAI.Erdos3.freeWordCoefficients line 77
  9. theorem OAI.Erdos3.freeWordCoefficients_word line 81
  10. theorem OAI.Erdos3.freeWordCoefficients_truncation line 87
  11. theorem OAI.Erdos3.freeWordCoefficients_embedding line 108
  12. theorem OAI.Erdos3.wordTruncation_homogeneous line 126
  13. theorem OAI.Erdos3.wordTruncation_freeLie_mem line 138
  14. def OAI.Erdos3.freeLieTruncation line 155
  15. theorem OAI.Erdos3.freeLieTruncation_expansion line 159
  16. theorem OAI.Erdos3.freeLieTruncation_associativeExpansion line 163
  17. theorem OAI.Erdos3.freeLieTruncation_idempotent line 169
  18. theorem OAI.Erdos3.freeLieTruncation_support_length line 174
  19. theorem OAI.Erdos3.lift_freeLieTruncation line 182
  20. def OAI.Erdos3.freeWordSplits line 199
  21. theorem OAI.Erdos3.mem_freeWordSplits line 204
  22. theorem OAI.Erdos3.freeWordSplits_card_le line 226
  23. theorem OAI.Erdos3.freeWordCoefficients_mul line 231
  24. def OAI.Erdos3.FreeCoefficientBound line 248
  25. theorem OAI.Erdos3.FreeCoefficientBound.mono line 256
  26. theorem OAI.Erdos3.FreeCoefficientBound.zero line 262
  27. theorem OAI.Erdos3.FreeCoefficientBound.word line 267
  28. theorem OAI.Erdos3.FreeCoefficientBound.one line 276
  29. theorem OAI.Erdos3.FreeCoefficientBound.neg line 279
  30. theorem OAI.Erdos3.FreeCoefficientBound.add_same line 285
  31. theorem OAI.Erdos3.FreeCoefficientBound.enlarge_denominator line 293
  32. theorem OAI.Erdos3.FreeCoefficientBound.smul line 302
  33. theorem OAI.Erdos3.FreeCoefficientBound.mul line 312
  34. theorem OAI.Erdos3.FreeCoefficientBound.pow line 343
  35. theorem OAI.Erdos3.FreeCoefficientBound.sum_finset line 350
  36. theorem OAI.Erdos3.FreeCoefficientBound.list_prod line 362
  37. theorem OAI.Erdos3.FreeCoefficientBound.rationalHeight line 370
  38. theorem OAI.Erdos3.commutatorTree_coefficient_bound line 394
  39. theorem OAI.Erdos3.commutatorTree_coefficient_height line 415
  40. theorem OAI.Erdos3.commutatorTree_coefficient_integral line 423