OAI/Combinatorics/Progressions/Sampling/SmoothPairPhysicalGrid.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.smoothPairKernelBaseCapline 11 - def
OAI.Erdos3.smoothPairKernelBaseLipline 15 - def
OAI.Erdos3.smoothPairKernelCapline 20 - def
OAI.Erdos3.smoothPairKernelLipline 23 - theorem
OAI.Erdos3.normalized_integer_pair_distline 27 - theorem
OAI.Erdos3.shiftedPairLocationKernel_capline 45 - theorem
OAI.Erdos3.shiftedPairLocationKernel_grid_errorline 57