OAI/Combinatorics/Progressions/Estimates/MaskedCenteredCounting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.maskedNormalized line 15
  2. theorem OAI.Erdos3.maskedNormalized_bounds line 18
  3. theorem OAI.Erdos3.maskedNormalized_score_le line 27
  4. theorem OAI.Erdos3.maskedNormalized_mean line 34
  5. theorem OAI.Erdos3.CyclicNiltestUpperComparison.masked line 65
  6. theorem OAI.Erdos3.CyclicNiltestUpperComparison.masked_mean line 84
  7. theorem OAI.Erdos3.exists_positive_progression_counting line 104
  8. theorem OAI.Erdos3.exists_masked_positive_counting line 164
  9. theorem OAI.Erdos3.consecutive_slopes_unit line 207
  10. theorem OAI.Erdos3.exists_positive_counting line 217
  11. theorem OAI.Erdos3.exists_masked_centered_counting line 256