OAI/Combinatorics/Progressions/Estimates/RelativePatchSourceTestFinBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.relativePatchSourceTest line 10
  2. theorem OAI.Erdos3.relativePatchSourceTest_integer line 15
  3. theorem OAI.Erdos3.relativePatchSourceTest_abs_le_one line 22
  4. theorem OAI.Erdos3.relativePatchSourceTest_mean line 35
  5. theorem OAI.Erdos3.relativePatchSourceTest_productive_data line 44
  6. theorem OAI.Erdos3.relativePatchSourceTest_fin_mean line 63
  7. theorem OAI.Erdos3.relativePatchSourceTest_fin_productive_data line 74
  8. theorem OAI.Erdos3.relativePatchSourceTest_fin_productive_data_of_box line 97
  9. theorem OAI.Erdos3.relativePatchSourceTrim_bounds line 111
  10. theorem OAI.Erdos3.relativePatchSourceGain_pos line 122