OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/KernelWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySharpWindow.kernelWindow line 25
2. lemma OAI.OrdinarySharpWindow.kernelWindow_integrable line 28
3. lemma OAI.OrdinarySharpWindow.kernel_box_integrable line 33
4. lemma OAI.OrdinarySharpWindow.box_kernel_comm line 40
5. lemma OAI.OrdinarySharpWindow.smooth_sharpWindow line 51
6. theorem OAI.OrdinarySharpWindow.sharp_l1_le_kernel line 92