OAI/Combinatorics/Progressions/Sampling/AllocatedGridlessEnvelopeCap.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.VectorPolynomial.allocatedGridJetScale_le_uniformline 19 - def
OAI.Erdos3.VectorPolynomial.allocatedGridlessEnvelopeCapline 66 - theorem
OAI.Erdos3.VectorPolynomial.allocatedIdealSiteEnvelope_le_invVolumeline 69 - theorem
OAI.Erdos3.VectorPolynomial.allocatedGridlessSiteEnvelope_abs_leline 94 - theorem
OAI.Erdos3.VectorPolynomial.allocatedGridlessEnvelopeCap_le_expline 141