OAI/Combinatorics/Progressions/Estimates/AllocatedFrozenBlockPMF.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedFrozenBlockPMF line 26
2. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetFactor_frozen_blocks line 38
3. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetDensity_frozen_blocks line 67