OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraEnergySum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite Cauchy summation of the actual additional logarithmic bins. The two per-bin estimates retain their separate small- and large-value costs, and the full bin count is absorbed by the proved power saving.

  1. lemma OAI.TwoPointCorrelations.mrt_product_energy_split line 15
  2. lemma OAI.TwoPointCorrelations.mrt_bin_sum_energy line 27
  3. lemma OAI.TwoPointCorrelations.mrt_extra_small_bin_cost line 36
  4. theorem OAI.TwoPointCorrelations.mrt_extra_coarse_energy line 67