OAI/Combinatorics/Progressions/Lattices/AffineKernelEndpointGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineCubeTuple line 15
  2. theorem OAI.Erdos3.affineCubeTuple_lipschitz line 18
  3. theorem OAI.Erdos3.affineCubeTuple_width_dist line 31
  4. theorem OAI.Erdos3.affineCubeTuple_integral_width_error line 43
  5. theorem OAI.Erdos3.affineCubeTuple_residue_riemann line 66
  6. def OAI.Erdos3.affineKernelContinuousPoint line 98
  7. def OAI.Erdos3.affineKernelDiscretePoint line 102
  8. theorem OAI.Erdos3.affineKernelContinuousPoint_lipschitz line 106
  9. theorem OAI.Erdos3.affineKernelEndpoint_dist_le line 128