OAI/Combinatorics/SumProduct/Alignment/RoughExtremal01.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RoughExtremalProgressions.APFree line 24
  2. def OAI.RoughExtremalProgressions.extremal line 28
  3. lemma OAI.RoughExtremalProgressions.le_extremal line 32
  4. lemma OAI.RoughExtremalProgressions.extremal_le line 37
  5. def OAI.RoughExtremalProgressions.blockResidues line 45
  6. lemma OAI.RoughExtremalProgressions.blockResidues_subset line 48
  7. lemma OAI.RoughExtremalProgressions.blockResidues_card line 54
  8. lemma OAI.RoughExtremalProgressions.mem_from_residue line 68
  9. lemma OAI.RoughExtremalProgressions.block_APFree line 76
  10. theorem OAI.RoughExtremalProgressions.card_le_extremal_blocks line 92
  11. theorem OAI.RoughExtremalProgressions.density_le_extremal line 116
  12. def OAI.RoughProgressionDensity.BadAt line 158
  13. def OAI.RoughProgressionDensity.blockOfProgression line 170
  14. lemma OAI.RoughProgressionDensity.rough_add_multiple line 189
  15. def OAI.RoughProgressionDensity.badIndices line 200
  16. lemma OAI.RoughProgressionDensity.mem_badIndices line 206
  17. lemma OAI.RoughProgressionDensity.no_bounded_AP line 215
  18. theorem OAI.RoughProgressionDensity.eventual_density_bound line 254