OAI/Combinatorics/Progressions/Probability/AllocatedAccuracyReferenceMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.referenceProxyMass_exp_bound line 14
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_retained_reference_mass line 57
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixed_reference_mass_bound line 155
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_primitive_reference_mass_bound line 319
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_certified_reference_mass_bound line 480
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_accuracy_reference_mass_bound line 655