OAI/Combinatorics/Progressions/Lattices/AffineModerateGeometricApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affinePrimitiveEnvelope line 12
  2. theorem OAI.Erdos3.affinePrimitiveEnvelope_one_le line 17
  3. theorem OAI.Erdos3.affinePrimitiveEnvelope_vector line 20
  4. theorem OAI.Erdos3.affinePrimitiveEnvelope_coefficient line 27
  5. theorem OAI.Erdos3.affinePrimitiveEnvelope_stride line 34
  6. theorem OAI.Erdos3.affineCube_geometric_approximation line 50
  7. theorem OAI.Erdos3.affineModerate_geometric_approximation line 137