OAI/Combinatorics/Progressions/Linear/RankQuotientHeightBudget.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_bounded_submodule_quotient_basis line 18
  2. theorem OAI.Erdos3.exists_submodule_quotient_basis_exp line 41
  3. def OAI.Erdos3.chosenBoundedSubmoduleBasis line 67
  4. theorem OAI.Erdos3.chosenBoundedSubmoduleBasis_height line 73
  5. theorem OAI.Erdos3.chosenBoundedSubmoduleBasis_range line 82
  6. theorem OAI.Erdos3.exists_bounded_submodule_basis_from_spanning line 99
  7. theorem OAI.Erdos3.exists_stepDrop_bounded_basis line 121
  8. def OAI.Erdos3.stepDropBracketHeight line 151
  9. theorem OAI.Erdos3.stepDrop_bracket_height line 155
  10. theorem OAI.Erdos3.stepDrop_basis_height_budget line 166
  11. theorem OAI.Erdos3.exists_stepDrop_basis_exp_height line 190
  12. def OAI.Erdos3.preimageBasisBudget line 223
  13. theorem OAI.Erdos3.preimageBasisBudget_nonneg line 226
  14. theorem OAI.Erdos3.exists_preimage_basis_logHeight line 231
  15. def OAI.Erdos3.rankQuotientLayerHeight line 293
  16. def OAI.Erdos3.rankQuotientFrequencyHeight line 296
  17. def OAI.Erdos3.rankQuotientHeight line 300
  18. theorem OAI.Erdos3.exists_bounded_rank_quotient_data line 306
  19. theorem OAI.Erdos3.chosenBasis_smul_coordinate_height line 419
  20. def OAI.Erdos3.homogeneousIntersectionSystem line 448
  21. theorem OAI.Erdos3.homogeneousIntersectionSystem_ker line 456
  22. theorem OAI.Erdos3.homogeneousIntersectionSystem_basis_height line 480
  23. def OAI.Erdos3.homogeneousIntersectionBasisHeight line 499
  24. theorem OAI.Erdos3.exists_homogeneousIntersection_basis line 502
  25. theorem OAI.Erdos3.rankQuotientHeight_le_exp line 540
  26. theorem OAI.Erdos3.dependentQuotientHeight_le_exp line 589