OAI/Combinatorics/Progressions/Estimates/AllocatedFixedScaleJointMarginal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_narrow_normalization line 15
2. theorem OAI.Erdos3.narrowTrimmedSpatial_site_width line 167
3. def OAI.Erdos3.narrowPhysicalSiteMap line 180
4. theorem OAI.Erdos3.narrowPhysicalSiteMap_cast line 193
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_narrow_oneSite_domination line 215
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixed_scale_centered_normalization line 393
7. def OAI.Erdos3.VectorPolynomial.AllocatedFixedScaleCenteredOneSiteStatement line 499
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixedScale_centered_oneSite_comparison line 567
9. def OAI.Erdos3.VectorPolynomial.AllocatedFixedScaleJointMarginalStatement line 694
10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixedScale_joint_marginal line 767