OAI/Combinatorics/Progressions/Estimates/PreparedCenteredModelMarginalData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.PreparedModularGeneralCenteredDetectionFreeTrimInterface line 70
2. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralCenteredDetectionFreeTrim_of_direct line 162
3. def OAI.Erdos3.VectorPolynomial.preparedCenteredMarginalExponent line 260
4. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredMarginalExponent_spec line 263
5. def OAI.Erdos3.VectorPolynomial.PreparedCenteredModelMarginalDataInterface line 327
6. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredModelMarginalData_of_direct line 455
7. def OAI.Erdos3.VectorPolynomial.PreparedCenteredModelMarginalProjectionInterface line 522
8. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredModelMarginalProjectionData_of_direct line 636
9. def OAI.Erdos3.VectorPolynomial.PreparedCenteredModelMarginalRadiusInterface line 679
10. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredModelMarginalRadiusInterface_of_projection line 794