OAI/Combinatorics/Progressions/Lattices/NormalizedResidueSpatialHaarBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.variableLengthZeroCube_pi_residue_disintegration line 13
2. theorem OAI.Erdos3.variableLengthZeroCube_pi_uniform_residue_error line 39
3. theorem OAI.Erdos3.variableLengthZeroCube_residue_slow_quadrature line 70
4. theorem OAI.Erdos3.integerBox_residue_spatial_riemann line 117
5. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.integerBox_frozenSingleSiteHaarReference_riemann line 157
6. theorem OAI.Erdos3.normalizedResidueSpatial_budget line 191
7. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.integerBox_frozenSingleSiteHaarReference_riemann_budget line 256