OAI/Combinatorics/Progressions/Lattices/ResidueAffineProfileLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.shiftedUnitProfile line 12
  2. theorem OAI.Erdos3.shiftedUnitProfile_nonneg line 15
  3. theorem OAI.Erdos3.shiftedUnitProfile_weight line 19
  4. theorem OAI.Erdos3.shiftedUnitProfile_mass line 27
  5. theorem OAI.Erdos3.shiftedUnitProfile_integral line 32
  6. theorem OAI.Erdos3.shiftedUnitProfile_lipschitz line 36
  7. theorem OAI.Erdos3.shiftedUnitProfile_cap line 40
  8. theorem OAI.Erdos3.shiftedUnitProfile_support line 45
  9. theorem OAI.Erdos3.coefficientPMF_shiftedUnitProfile line 55
  10. theorem OAI.Erdos3.shiftedUnitProfile_residue line 66
  11. theorem OAI.Erdos3.residueSmoothIndexPMF_affine line 78
  12. theorem OAI.Erdos3.residueProfileCenter_le_width line 92
  13. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_shifted_comparison line 102