OAI/Combinatorics/Progressions/Lattices/AllocatedTrimmedResidueTest.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_site_mass_bound line 11
2. theorem OAI.Erdos3.BooleanCubeKernel.physicalCenteredResidueMixture_site_error line 35
3. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_site_error line 73
4. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_coefficient_tail line 112
5. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_coefficient_tail_of_window_mass line 158
6. theorem OAI.Erdos3.BooleanCubeKernel.referenceErrorVolumeFactor_bound line 200
7. theorem OAI.Erdos3.VectorPolynomial.allocatedTrimmedSpatial_selected_site_test line 240