OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLinearKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite-height kernel bound measured at the natural short-window frequency scale. It preserves the linear first-prime-band cost.

  1. theorem OAI.TwoPointCorrelations.mrt_short_kernel_linear_height line 12
  2. lemma OAI.TwoPointCorrelations.mrt_linear_prefix_two_slopes line 96
  3. theorem OAI.TwoPointCorrelations.mrt_dyadic_kernel_linear_height line 114