OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogKernelQuarter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The short-window kernel needs spectral information only below one quarter of the polynomial length. The rest uses the unconditional mean square.

  1. theorem OAI.TwoPointCorrelations.mrt_dyadic_kernel_quarter_height line 13
  2. theorem OAI.TwoPointCorrelations.mrt_log_kernel_quarter_bound line 46