OAI/Combinatorics/Progressions/Probability/AllocatedPlateauPointMixture.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedConstantPointApproximation line 43
2. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPointMixture_error_of_tail line 48
3. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPointMixture_error line 69
4. def OAI.Erdos3.VectorPolynomial.allocatedResiduePlateauApproximation line 142
5. theorem OAI.Erdos3.VectorPolynomial.allocatedResiduePlateauApproximation_error_of_tail line 148
6. theorem OAI.Erdos3.VectorPolynomial.allocatedResiduePlateauApproximation_norm_le line 167
7. def OAI.Erdos3.VectorPolynomial.allocatedConstantPlateauApproximation line 194
8. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPlateauApproximation_error_of_tail line 200
9. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPlateauApproximation_error line 221
10. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPlateauApproximation_norm_le line 251