OAI/Combinatorics/Progressions/Estimates/NativeGraphSmallDifference.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Finset.addEnergy' line 14
  2. theorem OAI.Finset.addEnergy'_eq_div_energy line 20
  3. theorem OAI.Finset.cast_addEnergy' line 23
  4. def OAI.Erdos3.BSG.dconv line 45
  5. theorem OAI.Erdos3.BSG.dconv_eq_expect_add line 52
  6. theorem OAI.Erdos3.BSG.dconv_eq_expect_sub line 68
  7. theorem OAI.Erdos3.BSG.expect_dconv_mul line 76
  8. theorem OAI.Erdos3.BSG.expect_dconv line 82
  9. theorem OAI.Erdos3.BSG.dconv_indicator_one line 86
  10. theorem OAI.Erdos3.BSG.indicator_one_dconv_indicator_one_eq_dens line 91
  11. theorem OAI.Erdos3.BSG.indicator_one_dconv_indicator_one_eq_addConvolution_div line 97
  12. theorem OAI.Erdos3.BSG.expect_indicator_one_dconv_indicator_one line 102
  13. theorem OAI.Erdos3.BSG.expect_indicator_one_dconv_indicator_sq line 107
  14. theorem OAI.Erdos3.BSG.dconv_nonneg line 137
  15. theorem OAI.Erdos3.BSG.dconv_apply_nonneg line 141
  16. theorem OAI.Erdos3.BSG.dconv_pos line 144
  17. lemma OAI.Erdos3.BSG.oneOfPair_aux line 176
  18. def OAI.Erdos3.BSG.oneOfPair line 181
  19. lemma OAI.Erdos3.BSG.oneOfPair_subset line 184
  20. lemma OAI.Erdos3.BSG.mem_oneOfPair line 186
  21. lemma OAI.Erdos3.BSG.oneOfPair_bound_one line 189
  22. lemma OAI.Erdos3.BSG.oneOfPair_bound_two line 198
  23. lemma OAI.Erdos3.BSG.oneOfPair_bound line 214
  24. lemma OAI.Erdos3.BSG.quadruple_bound_c line 222
  25. lemma OAI.Erdos3.BSG.quadruple_bound_right line 234
  26. lemma OAI.Erdos3.BSG.claim_one line 247
  27. lemma OAI.Erdos3.BSG.claim_two line 251
  28. lemma OAI.Erdos3.BSG.claim_three line 269
  29. lemma OAI.Erdos3.BSG.claim_four line 284
  30. lemma OAI.Erdos3.BSG.claim_five line 308
  31. def OAI.Erdos3.BSG.choiceH line 313
  32. lemma OAI.Erdos3.BSG.choiceH_subset line 317
  33. lemma OAI.Erdos3.BSG.claim_six line 319
  34. lemma OAI.Erdos3.BSG.claim_seven line 334
  35. lemma OAI.Erdos3.BSG.claim_eight line 352
  36. lemma OAI.Erdos3.BSG.lemma_one line 369
  37. lemma OAI.Erdos3.BSG.lemma_one' line 397
  38. lemma OAI.Erdos3.BSG.quadruple_bound_other line 413
  39. lemma OAI.Erdos3.BSG.quadruple_bound_left line 425
  40. lemma OAI.Erdos3.BSG.quadruple_bound line 447
  41. lemma OAI.Erdos3.BSG.big_quadruple_bound line 458
  42. lemma OAI.Erdos3.BSG.BSG_aux line 482
  43. theorem OAI.Erdos3.BSG.balogSzemerediGowers line 504
  44. theorem OAI.Erdos3.BSG.BSG₂ line 514
  45. theorem OAI.Erdos3.BSG.BSG_self line 529
  46. theorem OAI.Erdos3.BSG.BSG_self' line 533
  47. theorem OAI.Erdos3.BSG.density_mul_le_iff_card_mul_le line 555
  48. theorem OAI.Erdos3.BSG.density_le_mul_iff_card_le_mul line 562
  49. theorem OAI.Erdos3.BSG.exists_large_subset_small_difference line 568
  50. theorem OAI.Erdos3.mem_additiveGraph_iff line 599
  51. theorem OAI.Erdos3.additiveGraph_image_fst line 608
  52. theorem OAI.Erdos3.exists_large_graph_subset_small_difference line 623
  53. theorem OAI.Erdos3.NativeRankRelation.CommonData.variable_coefficient_graph_energy line 663
  54. theorem OAI.Erdos3.NativeRankRelation.CommonData.variable_graph_small_difference line 683
  55. theorem OAI.Erdos3.NativeRankRelation.CommonData.rounded_graph_small_difference line 723
  56. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_rounded_graph_small_difference line 742