OAI/Combinatorics/Progressions/Estimates/SlicedPairAmplitude.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.SlicedProductBlock line 12
  2. structure OAI.Erdos3.SlicedProductBlock.Admissible line 23
  3. def OAI.Erdos3.SlicedProductBlock.prefixProduct line 29
  4. def OAI.Erdos3.SlicedProductBlock.value line 32
  5. def OAI.Erdos3.SlicedProductBlock.slope line 35
  6. def OAI.Erdos3.SlicedProductBlock.base line 38
  7. def OAI.Erdos3.SlicedProductBlock.volumeScale line 41
  8. theorem OAI.Erdos3.SlicedProductBlock.value_eq line 44
  9. theorem OAI.Erdos3.SlicedProductBlock.prefixProduct_continuous line 49
  10. theorem OAI.Erdos3.SlicedProductBlock.slope_continuous line 53
  11. theorem OAI.Erdos3.SlicedProductBlock.base_continuous line 56
  12. theorem OAI.Erdos3.SlicedProductBlock.volumeScale_pos line 59
  13. theorem OAI.Erdos3.SlicedProductBlock.prefixProduct_nonneg line 63
  14. theorem OAI.Erdos3.SlicedProductBlock.slope_lower line 68
  15. theorem OAI.Erdos3.SlicedProductBlock.volumeScale_lower line 81
  16. def OAI.Erdos3.SlicedProductBlock.pairScale line 106
  17. def OAI.Erdos3.SlicedProductBlock.pairWidth line 108
  18. theorem OAI.Erdos3.SlicedProductBlock.pairScale_pos line 111
  19. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_measurable line 114
  20. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_lower line 118
  21. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_pos line 133
  22. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_inverse_bound line 138
  23. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_inverse_integrable line 146
  24. def OAI.Erdos3.SlicedProductBlock.pairCap line 156
  25. theorem OAI.Erdos3.SlicedProductBlock.pairCap_pos line 159
  26. theorem OAI.Erdos3.SlicedProductBlock.pairWidth_inverse_integral_le line 162
  27. theorem OAI.Erdos3.SlicedProductBlock.pairCap_le_of_scale_lower line 171