OAI/Combinatorics/Progressions/Estimates/FreimanInverseLift.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FreimanModel.badMultipliers line 11
  2. lemma OAI.Erdos3.FreimanModel.mem_badMultipliers line 14
  3. lemma OAI.Erdos3.FreimanModel.card_badMultipliers_le line 18
  4. lemma OAI.Erdos3.FreimanModel.intCast_zmod_ne_zero_of_natAbs_lt line 50
  5. lemma OAI.Erdos3.FreimanModel.card_biUnion_badMultipliers_le line 60
  6. lemma OAI.Erdos3.FreimanModel.multiplier_union_card_lt line 72
  7. theorem OAI.Erdos3.FreimanModel.exists_good_multiplier line 83
  8. lemma OAI.Erdos3.FreimanModel.multiset_sum_mem_nsmul line 134
  9. def OAI.Erdos3.FreimanModel.ruzsaRepresentative line 145
  10. def OAI.Erdos3.FreimanModel.ruzsaColor line 148
  11. def OAI.Erdos3.FreimanModel.ruzsaModelMap line 151
  12. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentative_lt line 154
  13. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentative_cast line 158
  14. lemma OAI.Erdos3.FreimanModel.ruzsaColor_lt line 162
  15. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentative_sub_lt_of_color_eq line 175
  16. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentative_bounds_of_color_eq line 203
  17. def OAI.Erdos3.FreimanModel.ruzsaRepresentativeSum line 217
  18. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentativeSum_bounds line 221
  19. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentativeSum_sub_abs_lt line 247
  20. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentativeSum_cast line 274
  21. lemma OAI.Erdos3.FreimanModel.ruzsaModelMap_sum line 287
  22. lemma OAI.Erdos3.FreimanModel.ruzsaBlockWidth_lt line 297
  23. lemma OAI.Erdos3.FreimanModel.ruzsaRepresentativeSum_sub_cast line 304
  24. lemma OAI.Erdos3.FreimanModel.ruzsaModelMap_sum_eq_iff_dvd line 313
  25. lemma OAI.Erdos3.FreimanModel.zmod_val_eq_natAbs_of_nonneg line 328
  26. lemma OAI.Erdos3.FreimanModel.int_natAbs_lt_of_neg_lt_and_lt line 337
  27. lemma OAI.Erdos3.FreimanModel.ruzsaModelMap_multiset_sum_eq_iff line 351
  28. theorem OAI.Erdos3.FreimanModel.isAddFreimanIso_ruzsaModelMap line 443
  29. lemma OAI.Erdos3.FreimanModel.exists_nonempty_large_color_fiber line 486
  30. lemma OAI.Erdos3.FreimanModel.exists_nonempty_large_color_fiber_mul line 509
  31. theorem OAI.Erdos3.FreimanModel.exists_large_cyclic_freiman_model line 540
  32. structure OAI.Erdos3.FreimanModel.FourfoldPresentation line 614
  33. def OAI.Erdos3.FreimanModel.FourfoldPresentation.eval line 624
  34. def OAI.Erdos3.FreimanModel.FourfoldPresentation.Mem line 627
  35. lemma OAI.Erdos3.FreimanModel.mem_two_nsmul_sub_two_nsmul_iff line 635
  36. def OAI.Erdos3.FreimanModel.defaultFourfoldPresentation line 660
  37. def OAI.Erdos3.FreimanModel.selectedFourfoldPresentation line 665
  38. lemma OAI.Erdos3.FreimanModel.selectedFourfoldPresentation_spec line 672
  39. def OAI.Erdos3.FreimanModel.fourfoldMapValue line 680
  40. lemma OAI.Erdos3.FreimanModel.fourfold_sub_eq_iff_cross_add line 683
  41. lemma OAI.Erdos3.FreimanModel.add_fourfold_sub_eq_iff_cross_add line 700
  42. lemma OAI.Erdos3.FreimanModel.fourfoldMapValue_eq_iff_eval_eq line 726
  43. def OAI.Erdos3.FreimanModel.freimanFourfoldLift line 767
  44. lemma OAI.Erdos3.FreimanModel.freimanFourfoldLift_eq_of_presentation line 771
  45. lemma OAI.Erdos3.FreimanModel.freimanFourfoldLift_mem_two_nsmul_sub_two_nsmul line 781
  46. theorem OAI.Erdos3.FreimanModel.freimanFourfoldLift_injOn line 792
  47. lemma OAI.Erdos3.FreimanModel.freimanFourfoldLift_add_eq_add line 803
  48. theorem OAI.Erdos3.FreimanModel.freimanFourfoldLift_isAddFreimanIso line 869
  49. theorem OAI.Erdos3.FreimanModel.exists_fourfold_lift_of_eight_iso line 899