OAI/Combinatorics/Progressions/Estimates/BinaryTupleSorting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.binary_eq_zero_of_ne_one line 12
  2. theorem OAI.Erdos3.binary_eq_one_of_ne_zero line 19
  3. def OAI.Erdos3.binaryZeroCount line 26
  4. def OAI.Erdos3.binarySorted line 29
  5. theorem OAI.Erdos3.binaryZeroCount_comp line 31
  6. theorem OAI.Erdos3.binarySorted_comp line 35
  7. theorem OAI.Erdos3.binarySorted_threshold line 39
  8. def OAI.Erdos3.zeroFixedPermutation line 61
  9. theorem OAI.Erdos3.binarySorted_tail line 73