OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SmoothCofactorHarmonic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySmoothDampedFamily.smoothCofactorHarmonic line 23
2. lemma OAI.OrdinarySmoothDampedFamily.continuous_smoothDamped line 27
3. lemma OAI.OrdinarySmoothDampedFamily.smoothCofactorHarmonic_integral line 34
4. theorem OAI.OrdinarySmoothDampedFamily.uniform_smooth_cofactor_harmonic line 54