OAI/Combinatorics/Progressions/Probability/AllocatedRecenteredActualMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_recentered_certified_mass_bound line 18
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_recentered_accuracy_mass_bound line 215
3. theorem OAI.Erdos3.VectorPolynomial.exists_uniform_allocated_recentered_actual_mass line 430