OAI/Combinatorics/Progressions/Linear/RankPreparationSizes.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.rankCutDirectionHeight line 14
  2. theorem OAI.Erdos3.VectorPolynomial.integerPolynomialQuotient_eval line 18
  3. theorem OAI.Erdos3.VectorPolynomial.exists_rankPreparationStep line 30
  4. structure OAI.Erdos3.RankPreparationLayer line 117
  5. def OAI.Erdos3.RankPreparationLayer.space line 136
  6. def OAI.Erdos3.RankPreparationLayer.rank line 139
  7. def OAI.Erdos3.RankPreparationLayer.Valid line 141
  8. theorem OAI.Erdos3.RankPreparationLayer.Valid.mono_height line 147
  9. def OAI.Erdos3.RankPreparationLayer.value line 151
  10. def OAI.Erdos3.RankPreparationLayer.reindex line 154
  11. theorem OAI.Erdos3.RankPreparationLayer.reindex_space line 157
  12. theorem OAI.Erdos3.RankPreparationLayer.reindex_rank line 160
  13. theorem OAI.Erdos3.RankPreparationLayer.Valid.reindex line 163
  14. theorem OAI.Erdos3.RankPreparationLayer.reindex_value line 169
  15. def OAI.Erdos3.RankPreparationLayer.cut line 174
  16. theorem OAI.Erdos3.RankPreparationLayer.cut_space line 187
  17. theorem OAI.Erdos3.RankPreparationLayer.Valid.cut line 191
  18. theorem OAI.Erdos3.RankPreparationLayer.cut_rank_lt line 203
  19. def OAI.Erdos3.RankPreparationLayer.appendLine line 210
  20. theorem OAI.Erdos3.RankPreparationLayer.appendLine_space line 223
  21. theorem OAI.Erdos3.RankPreparationLayer.appendLine_rank line 229
  22. theorem OAI.Erdos3.RankPreparationLayer.Valid.appendLine line 236
  23. theorem OAI.Erdos3.RankPreparationLayer.appendLine_value line 251
  24. def OAI.Erdos3.RankPreparationLayer.empty line 260
  25. theorem OAI.Erdos3.RankPreparationLayer.empty_valid line 272
  26. theorem OAI.Erdos3.RankPreparationLayer.empty_rank line 286
  27. theorem OAI.Erdos3.RankPreparationLayer.empty_value line 291
  28. def OAI.Erdos3.RankPreparationLayer.initial line 298
  29. theorem OAI.Erdos3.RankPreparationLayer.initial_space line 311
  30. theorem OAI.Erdos3.RankPreparationLayer.initial_valid line 329
  31. theorem OAI.Erdos3.RankPreparationLayer.initial_rank line 345
  32. theorem OAI.Erdos3.RankPreparationLayer.initial_value line 352
  33. theorem OAI.Erdos3.VectorPolynomial.rankCutDirectionHeight_le_exp line 367
  34. abbrev OAI.Erdos3.RankPreparationFamily line 439
  35. def OAI.Erdos3.RankPreparationFamily.value line 445
  36. def OAI.Erdos3.RankPreparationFamily.potential line 448
  37. def OAI.Erdos3.RankPreparationFamily.reindex line 451
  38. theorem OAI.Erdos3.RankPreparationFamily.reindex_potential line 454
  39. theorem OAI.Erdos3.RankPreparationFamily.reindex_value line 457
  40. def OAI.Erdos3.RankPreparationFamily.descend line 464
  41. theorem OAI.Erdos3.RankPreparationFamily.descend_potential line 471
  42. theorem OAI.Erdos3.RankPreparationFamily.descend_valid line 494
  43. theorem OAI.Erdos3.RankPreparationFamily.sum_replace_two line 516
  44. theorem OAI.Erdos3.RankPreparationFamily.descend_value line 533
  45. def OAI.Erdos3.RankPreparationFamily.absorb line 555
  46. theorem OAI.Erdos3.RankPreparationFamily.absorb_potential line 559
  47. theorem OAI.Erdos3.RankPreparationFamily.absorb_valid line 572
  48. theorem OAI.Erdos3.RankPreparationFamily.sum_replace_one line 586
  49. theorem OAI.Erdos3.RankPreparationFamily.absorb_value line 598
  50. theorem OAI.Erdos3.RankPreparationFamily.exists_descend_slice_step line 626
  51. theorem OAI.Erdos3.RankPreparationFamily.exists_absorb_slice_step line 709
  52. def OAI.Erdos3.RankPreparationFamily.Sized line 808
  53. theorem OAI.Erdos3.RankPreparationFamily.Sized.mono line 812
  54. theorem OAI.Erdos3.RankPreparationFamily.Sized.reindex line 818
  55. theorem OAI.Erdos3.RankPreparationFamily.copy_power_step line 821
  56. theorem OAI.Erdos3.RankPreparationFamily.Sized.descend line 827
  57. theorem OAI.Erdos3.RankPreparationFamily.Sized.absorb line 861
  58. theorem OAI.Erdos3.RankPreparationFamily.Sized.uniform line 874