OAI/Combinatorics/Progressions/Geometry/NormalizedTwistSpatialPartition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenTorus line 13
2. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_frozenTorus_le line 18
3. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenTorus_lipschitz line 26
4. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenTorus_spatial_error line 41
5. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenSpatialEval line 57
6. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.eval_sub_frozenSpatialEval line 63
7. def OAI.Erdos3.VectorPolynomial.normalizedVertexRadius line 81
8. theorem OAI.Erdos3.VectorPolynomial.normalizedVertexRadius_nonneg line 85
9. theorem OAI.Erdos3.VectorPolynomial.normalized_physicalVertex_norm_le line 89
10. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_eval_sub_frozenSpatialEval line 121
11. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_eval_sub_frozenSpatialEval_zero line 147
12. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.spatialPartitionLaw line 176
13. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.spatialPartitionLaw_near line 186
14. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.spatialPartition_error line 197