OAI/Combinatorics/Progressions/Estimates/FactoredPositiveShiftContradiction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_avoiding_exceptional_family line 15
  2. theorem OAI.Erdos3.abs_expect_mul_le_cap line 46
  3. theorem OAI.Erdos3.signed_shift_weight_bound line 56
  4. theorem OAI.Erdos3.fixed_list_error_cost line 70
  5. theorem OAI.Erdos3.larger_slack_weighted_term_le line 86
  6. theorem OAI.Erdos3.partition_expansion_error_small line 105
  7. theorem OAI.Erdos3.exists_partition_expansion_precision line 135
  8. theorem OAI.Erdos3.partition_expansion_precision_properties line 145
  9. theorem OAI.Erdos3.density_parameter_le_one line 159
  10. theorem OAI.Erdos3.positive_shift_mean_cap line 166
  11. theorem OAI.Erdos3.fixed_list_log_components line 186
  12. theorem OAI.Erdos3.fixed_list_contradiction_of_pair_bounds line 209
  13. theorem OAI.Erdos3.fixed_list_working_budget_suffices line 266
  14. theorem OAI.Erdos3.cyclic_fixed_list_contradiction line 333
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_partition_expansion line 407
  16. def OAI.Erdos3.CyclicShiftComparison line 431
  17. theorem OAI.Erdos3.exists_degree_one_cyclicShiftComparison line 443
  18. theorem OAI.Erdos3.exists_cyclic_fixed_list_power line 460
  19. theorem OAI.Erdos3.exists_cyclic_partition_expansion_contradiction line 538
  20. theorem OAI.Erdos3.exists_native_partition_expansion_contradiction line 619
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prepared_higher_shift_contradiction line 681
  22. theorem OAI.Erdos3.PositiveShiftBasis.exists_factored_positive_shift_contradiction line 746