OAI/Combinatorics/Progressions/Estimates/NormalizedIntervalWindow.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.intervalWindow line 11
  2. theorem OAI.Erdos3.intervalWindow_mem_Icc line 14
  3. theorem OAI.Erdos3.intervalWindow_measurable line 17
  4. theorem OAI.Erdos3.intervalWindow_integrable line 20
  5. theorem OAI.Erdos3.integral_intervalWindow line 25
  6. theorem OAI.Erdos3.interval_separation line 30
  7. theorem OAI.Erdos3.intervalWindow_difference_le line 39
  8. theorem OAI.Erdos3.intervalWindow_integral_difference_le line 63
  9. theorem OAI.Erdos3.intervalWindow_translation_le line 80
  10. def OAI.Erdos3.normalizedIntervalWindow line 95
  11. theorem OAI.Erdos3.normalizedIntervalWindow_nonneg line 98
  12. theorem OAI.Erdos3.normalizedIntervalWindow_le line 101
  13. theorem OAI.Erdos3.normalizedIntervalWindow_integrable line 105
  14. theorem OAI.Erdos3.normalizedIntervalWindow_measurable line 108
  15. theorem OAI.Erdos3.normalizedIntervalWindow_mass line 111
  16. theorem OAI.Erdos3.normalizedIntervalWindow_translation_le line 117