OAI/Combinatorics/Progressions/Estimates/MarkedShiftGeneratorBounds.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.markedShiftSubalgebra line 15
  2. theorem OAI.Erdos3.markedShiftSubalgebra_contains_direction line 36
  3. theorem OAI.Erdos3.markedShiftSubalgebra_contains_polynomial line 40
  4. def OAI.Erdos3.markedShiftFiltration line 46
  5. theorem OAI.Erdos3.markedShift_lowerCentralSeries_eq_bot line 51
  6. def OAI.Erdos3.markedShiftPolynomialSubmodule line 69
  7. def OAI.Erdos3.markedShiftSecondIdeal line 85
  8. abbrev OAI.Erdos3.MarkedShiftQuotient line 108
  9. theorem OAI.Erdos3.markedShiftQuotient_lowerCentralSeries_eq_bot line 111
  10. abbrev OAI.Erdos3.MarkedShiftQuotientGroup line 117
  11. def OAI.Erdos3.markedShiftEval line 121
  12. def OAI.Erdos3.markedShiftBiLayer line 140
  13. theorem OAI.Erdos3.markedShiftBiLayer_antitone line 157
  14. theorem OAI.Erdos3.markedShiftBiLayer_zero line 164
  15. theorem OAI.Erdos3.markedPolynomialLayer_shiftDerivative line 171
  16. theorem OAI.Erdos3.markedShiftBiLayer_lie_mem line 185
  17. theorem OAI.Erdos3.markedShiftBiLayer_eq_polynomialSubmodule line 202
  18. theorem OAI.Erdos3.markedShiftBiLayer_second line 211
  19. theorem OAI.Erdos3.markedShiftBiLayer_positive line 215
  20. theorem OAI.Erdos3.markedShiftBiLayer_degree_terminal line 239
  21. def OAI.Erdos3.markedShiftDirection line 270
  22. theorem OAI.Erdos3.markedShiftDirection_lie_left line 273
  23. theorem OAI.Erdos3.markedShiftDirection_lie_right line 284
  24. theorem OAI.Erdos3.markedShiftDirection_double_lie_mem line 287
  25. def OAI.Erdos3.markedQuotientDirection line 296
  26. theorem OAI.Erdos3.markedQuotientDirection_double_lie line 299
  27. theorem OAI.Erdos3.markedQuotientDirection_conjugation line 306
  28. theorem OAI.Erdos3.markedShiftQuotient_finiteDimensional line 329
  29. theorem OAI.Erdos3.markedShiftQuotient_finrank_le line 339
  30. def OAI.Erdos3.markedPolynomialGeneratorFamily line 364
  31. theorem OAI.Erdos3.markedPolynomialGeneratorFamily_span line 370
  32. def OAI.Erdos3.markedShiftLayerPolynomialMap line 383
  33. def OAI.Erdos3.markedShiftDirectionMap line 401
  34. abbrev OAI.Erdos3.MarkedShiftGeneratorIndex line 407
  35. def OAI.Erdos3.markedShiftGenerator line 411
  36. theorem OAI.Erdos3.markedShiftGenerator_mem line 417
  37. theorem OAI.Erdos3.markedShiftGenerator_span line 427
  38. def OAI.Erdos3.markedShiftTranslate line 482
  39. theorem OAI.Erdos3.markedShiftTranslate_left line 502
  40. theorem OAI.Erdos3.markedShiftTranslate_right line 505
  41. theorem OAI.Erdos3.markedShiftEval_translate line 508
  42. theorem OAI.Erdos3.markedShiftTranslate_second_mem line 513
  43. theorem OAI.Erdos3.markedShiftTranslate_first_order line 518
  44. theorem OAI.Erdos3.markedShiftTranslate_quotient line 529
  45. theorem OAI.Erdos3.markedShiftTranslate_conjugation line 539
  46. def OAI.Erdos3.markedQuotientTranslate line 547
  47. theorem OAI.Erdos3.markedQuotientTranslate_map line 555
  48. theorem OAI.Erdos3.markedQuotientTranslate_first_order line 559
  49. def OAI.Erdos3.markedShiftQuotientLayer line 575
  50. theorem OAI.Erdos3.markedShiftQuotientLayer_antitone line 580
  51. theorem OAI.Erdos3.markedShiftQuotientLayer_zero line 585
  52. theorem OAI.Erdos3.markedShiftQuotientLayer_lie_mem line 590
  53. theorem OAI.Erdos3.markedShiftQuotientLayer_eq_bot_of_le line 600
  54. theorem OAI.Erdos3.markedShiftQuotientLayer_terminal line 608
  55. theorem OAI.Erdos3.markedShiftQuotientLayer_positive line 630
  56. theorem OAI.Erdos3.markedShiftQuotientLayer_total_one line 638
  57. theorem OAI.Erdos3.finiteMarkedPolynomialValues_coefficient_height line 661
  58. theorem OAI.Erdos3.markedShiftGenerator_coordinate_height line 688
  59. theorem OAI.Erdos3.exists_markedShiftLayer_bounded_basis line 713