OAI/Combinatorics/Progressions/Estimates/CommonCoefficientFourAnnihilators.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fourBasisVectors line 13
  2. theorem OAI.Erdos3.fourBasisVectors_apply line 18
  3. theorem OAI.Erdos3.fourBasisVectors_span line 31
  4. theorem OAI.Erdos3.fourCommonModulo_eq_sup line 44
  5. theorem OAI.Erdos3.fourCommonGenerators_span line 66
  6. def OAI.Erdos3.fourBalanceProjection line 88
  7. theorem OAI.Erdos3.fourBalanceProjection_apply line 91
  8. theorem OAI.Erdos3.fourBalanceProjection_image line 97
  9. theorem OAI.Erdos3.fourBalancedGenerators_span line 122
  10. theorem OAI.Erdos3.exists_bounded_four_annihilator line 138
  11. theorem OAI.Erdos3.fourPetalSpace_eq_inf_ker line 170
  12. theorem OAI.Erdos3.exists_bounded_refined_four_annihilator line 180
  13. theorem OAI.Erdos3.fourBasisVectors_logHeight line 218
  14. theorem OAI.Erdos3.fourBalancedGenerators_logHeight line 231
  15. theorem OAI.Erdos3.exists_fourCommonModulo_basis_logHeight line 244
  16. theorem OAI.Erdos3.exists_fourBalancedDependent_basis_logHeight line 259
  17. def OAI.Erdos3.fourRefinementBasisBudget line 279
  18. def OAI.Erdos3.fourRefinementAnnihilatorBudget line 282
  19. theorem OAI.Erdos3.fourRefinementBasisBudget_nonneg line 285
  20. theorem OAI.Erdos3.fourRefinementAnnihilatorBudget_nonneg line 289
  21. theorem OAI.Erdos3.fourRefinementBasisBudget_bound line 295
  22. theorem OAI.Erdos3.fourRefinementAnnihilatorBudget_bound line 305
  23. theorem OAI.Erdos3.four_submodule_finrank_le line 317
  24. theorem OAI.Erdos3.exists_fourRefinedRelation_basis_logHeight line 326
  25. theorem OAI.Erdos3.exists_fourRefinedRelation_annihilator line 375
  26. theorem OAI.Erdos3.exists_fourRefinedRelation_correction line 423
  27. def OAI.Erdos3.coefficientFourHeightBudget line 504
  28. theorem OAI.Erdos3.coefficientFourHeightBudget_nonneg line 506
  29. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficientFour_generators line 527
  30. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficientFour_basis line 579
  31. def OAI.Erdos3.coefficientFourAnnihilatorBudget line 606
  32. theorem OAI.Erdos3.coefficientFourAnnihilatorBudget_nonneg line 609
  33. theorem OAI.Erdos3.coefficientFourAnnihilatorBudget_bound line 615
  34. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_coefficientFour_annihilator line 638
  35. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_controlled_coefficientFour_annihilator line 662