OAI/Combinatorics/Progressions/Estimates/AllocatedActivePlateauAverage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedSelectedConditionalError line 71
2. theorem OAI.Erdos3.VectorPolynomial.allocatedSelectedConditionalError_bound line 84
3. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateau_haar_error line 191
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_site_haar_error line 313
5. def OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProfile line 391
6. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProfile_measurable line 418
7. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePlateauProfile_error line 427
8. def OAI.Erdos3.VectorPolynomial.allocatedActiveSiteProfile line 475
9. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteProfile_measurable line 499
10. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteProfile_error line 508
11. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedActivePlateau_residue_approximation line 597