OAI/Combinatorics/Progressions/Geometry/SampledCommonBox.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.commonStrideCount_exp_bound line 15
  2. theorem OAI.Erdos3.exists_dense_box_inner_family line 26
  3. def OAI.Erdos3.IsDenseCommonStrideBox line 99
  4. theorem OAI.Erdos3.IsDenseCommonStrideBox.nonempty line 105
  5. theorem OAI.Erdos3.exists_finite_site_box_inner_family line 111
  6. theorem OAI.Erdos3.commonStridePoint_coordinateEquiv line 152
  7. theorem OAI.Erdos3.commonStrideIndex_coordinateEquiv line 158
  8. theorem OAI.Erdos3.commonStrideBox_map_coordinateEquiv line 164
  9. theorem OAI.Erdos3.commonStrideBox_image_coordinateEquiv line 182
  10. theorem OAI.Erdos3.IsDenseCommonStrideBox.coordinateEquiv line 191
  11. theorem OAI.Erdos3.IsDenseCommonStrideBox.coordinateEquiv_map line 202
  12. def OAI.Erdos3.denseBoxGowersTransferCost line 220
  13. theorem OAI.Erdos3.denseBox_gowers_transfer line 223
  14. theorem OAI.Erdos3.exists_common_sampled_box line 287