OAI/Combinatorics/Progressions/Estimates/AllocatedCoveredHaarTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredDeck_relabel line 48
2. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientCover_density line 79
3. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredHaar_law line 93
4. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredHaar_integral line 100
5. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredHaar_finite_mean line 116
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredDensity_finite_mean line 125