OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SmoothDamped.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySmoothDampedFamily.smoothDamped line 23
2. lemma OAI.OrdinarySmoothDampedFamily.factored_mul_iff line 26
3. lemma OAI.OrdinarySmoothDampedFamily.smoothDamped_oneBounded line 33
4. lemma OAI.OrdinarySmoothDampedFamily.smoothDamped_multiplicative line 42
5. lemma OAI.OrdinarySmoothDampedFamily.smoothDamped_one line 50
6. lemma OAI.OrdinarySmoothDampedFamily.smooth_distanceSq_lower line 60
7. abbrev OAI.OrdinarySmoothDampedFamily.Parameters line 93
8. def OAI.OrdinarySmoothDampedFamily.family line 95
9. theorem OAI.OrdinarySmoothDampedFamily.family_divergence line 98