OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Smooth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySharpWindow.smooth line 24
2. lemma OAI.OrdinarySharpWindow.smooth_joint_integrable line 27
3. lemma OAI.OrdinarySharpWindow.smooth_integrable line 32
4. theorem OAI.OrdinarySharpWindow.smooth_error_l1 line 36
5. lemma OAI.OrdinarySharpWindow.smooth_l1_le line 84