OAI/NumberTheory/Ostmann/Quadratic/QuadraticOddKernelCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact finite cutoff in the odd-squarefree frequency variable

  1. theorem OAI.Ostmann.quadraticOddKernel_val_injective line 13
  2. theorem OAI.Ostmann.quadratic_odd_kernel_cutoff line 18
  3. theorem OAI.Ostmann.quadratic_odd_kernel_split line 47