OAI/Combinatorics/Progressions/Estimates/RelativeCoefficientGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integerProgressionSupport_one line 9
  2. structure OAI.Erdos3.RelativeProgression line 13
  3. def OAI.Erdos3.RelativeProgression.canonicalStep line 27
  4. def OAI.Erdos3.RelativeProgression.width line 29
  5. theorem OAI.Erdos3.RelativeProgression.canonicalStep_pos line 31
  6. theorem OAI.Erdos3.RelativeProgression.canonical_support line 37
  7. theorem OAI.Erdos3.RelativeProgression.length_pos line 44
  8. theorem OAI.Erdos3.RelativeProgression.width_pos line 50
  9. theorem OAI.Erdos3.RelativeProgression.geometric_bounds line 52
  10. def OAI.Erdos3.RelativeProgression.cubeSlice line 81
  11. theorem OAI.Erdos3.RelativeProgression.cubeSlice_nonempty line 83
  12. theorem OAI.Erdos3.relativeProgression_family_bounds line 100
  13. theorem OAI.Erdos3.RelativeProgression.parent_le_index_length line 143
  14. theorem OAI.Erdos3.RelativeProgression.root_bounds line 151
  15. theorem OAI.Erdos3.RelativeProgression.coefficient_radius_bound line 157
  16. theorem OAI.Erdos3.relativeModerate_family_bounds line 165