OAI/Combinatorics/Progressions/Geometry/CoefficientSquareSpatialBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.coefficientErrorVolumeLog line 13
2. def OAI.Erdos3.coefficientErrorSpatialLog line 15
3. theorem OAI.Erdos3.coefficientErrorSpatialLog_nonneg line 18
4. theorem OAI.Erdos3.coefficientErrorPeriod_exp_sq line 24
5. theorem OAI.Erdos3.referenceErrorVolumeFactor_exp_bound line 31
6. theorem OAI.Erdos3.coarseReferenceMassConstant_exp_bound line 63
7. theorem OAI.Erdos3.coefficientErrorSpatialFactor_exp_bound line 77
8. theorem OAI.Erdos3.spatialWindowFactor_le_referenceFactor line 125
9. theorem OAI.Erdos3.coefficientSquareSpatial_cost line 138