OAI/Combinatorics/Progressions/Estimates/FourBalancedRelations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fourAlternatingMap line 11
  2. theorem OAI.Erdos3.fourAlternatingMap_apply line 14
  3. def OAI.Erdos3.fourCommonModulo line 17
  4. theorem OAI.Erdos3.mem_fourCommonModulo line 21
  5. def OAI.Erdos3.fourBalancedDependent line 25
  6. theorem OAI.Erdos3.mem_fourBalancedDependent line 28
  7. theorem OAI.Erdos3.fourBalancedDependent_le_common line 32
  8. def OAI.Erdos3.fourRefinedRelation line 39
  9. theorem OAI.Erdos3.fourRefinedRelation_le_common line 43
  10. theorem OAI.Erdos3.fourBalancedDependent_le_refined line 47
  11. def OAI.Erdos3.fourPetalSpace line 51
  12. theorem OAI.Erdos3.mem_fourPetalSpace line 54
  13. theorem OAI.Erdos3.fourPetalSpace_le_first line 57
  14. theorem OAI.Erdos3.fourAlternatingMap_mem_dependent line 62