OAI/Combinatorics/Progressions/Lattices/AffineOneSiteNormalizedLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.selectedResidueDensityPMF_test_le line 11
2. theorem OAI.Erdos3.selectedResidueDensityPMF_test_le_of_complex line 41
3. theorem OAI.Erdos3.selectedResidueSmoothPMF_test_le_of_complex line 66
4. def OAI.Erdos3.BooleanCubeKernel.physicalAffineSite line 101
5. theorem OAI.Erdos3.BooleanCubeKernel.integerSiteValue_oneSite line 106
6. theorem OAI.Erdos3.BooleanCubeKernel.layeredSiteWeight_physical line 116
7. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_oneSite_density_error line 133
8. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_oneSite_density_comparison line 186
9. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_oneSite_test_domination line 257
10. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_translated_oneSite_density_comparison line 342
11. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_oneSite_normalized_domination line 432