OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWindowKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A uniform Fourier kernel for all relative windows up to a given size. No multiplicativity assumptions enter this finite analytic estimate.

  1. def OAI.TwoPointCorrelations.mrtWindowKernel line 13
  2. lemma OAI.TwoPointCorrelations.mrt_log_dirichlet_norm line 16
  3. lemma OAI.TwoPointCorrelations.mrt_log_dirichlet_continuous line 27
  4. lemma OAI.TwoPointCorrelations.mrt_window_kernel_integrable line 32
  5. lemma OAI.TwoPointCorrelations.mrt_window_frequency_integrable line 49
  6. theorem OAI.TwoPointCorrelations.mrt_log_window_uniform_kernel line 66
  7. lemma OAI.TwoPointCorrelations.mrt_log_window_joint_measurable line 83
  8. lemma OAI.TwoPointCorrelations.mrt_log_window_energy_measurable line 94
  9. lemma OAI.TwoPointCorrelations.mrt_log_window_energy_intervalIntegrable line 99
  10. theorem OAI.TwoPointCorrelations.mrt_log_window_kernel_average line 112