OAI/Combinatorics/Progressions/Linear/AllocatedKernelSiteMask.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedKernelSiteLift line 25
2. def OAI.Erdos3.VectorPolynomial.allocatedKernelSiteMask line 34
3. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteMask_reconstructed line 41
4. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteMask_bound line 67
5. theorem OAI.Erdos3.VectorPolynomial.allocatedLongProfileDensity_site_mask line 76
6. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteMask_expansion line 89
7. theorem OAI.Erdos3.VectorPolynomial.allocatedKernelSiteMask_coefficient_sum line 104