OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/AccuracyCancel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryUniformWidth.accuracy_cancel line 25
2. lemma OAI.OrdinaryUniformWidth.accuracy_sq_cancel line 29
3. lemma OAI.OrdinaryUniformWidth.approxBound_large_K line 33
4. lemma OAI.OrdinaryUniformWidth.approxBound_large_H line 36
5. lemma OAI.OrdinaryUniformWidth.shortWidth_large_H line 42
6. lemma OAI.OrdinaryUniformWidth.shortWidth_large_smooth line 48
7. lemma OAI.OrdinaryUniformWidth.major_radius line 55
8. lemma OAI.OrdinaryUniformWidth.minor_radius line 71
9. lemma OAI.OrdinaryUniformWidth.smooth_loss_small line 79