OAI/Combinatorics/Progressions/Fourier/AllocatedSupportedResidueSpectrum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSources_volume line 35
2. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveResidueSpectrum_tail line 45
3. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalGridSpectrum_tail line 116
4. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalGridSpectrum_absolute_cap line 157
5. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalGridSpectrum_cover_card line 182
6. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSpectrum_tail line 227
7. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedResidueSpectrum_absolute_cap line 251