OAI/NumberTheory/TwoPoint/Fourier/MajorArcCorrectedRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The correction and character factors fit the exact error exponents of corrected MRT Theorem 1.7 at the common parameter.

  1. lemma OAI.TwoPointCorrelations.major_arc_inverse_parameter_error line 12
  2. theorem OAI.TwoPointCorrelations.major_arc_corrected_published_rate line 25
  3. lemma OAI.TwoPointCorrelations.major_arc_rate_volume line 83