OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraFactorization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complete additional-prime factorization of the actual typical polynomial. The missing-band, prime-square and bin-boundary errors are summed once, independently of the frequency classes.

  1. def OAI.TwoPointCorrelations.mrtExtraCoarsePolynomial line 15
  2. lemma OAI.TwoPointCorrelations.mrt_extra_coarse_continuous line 23
  3. theorem OAI.TwoPointCorrelations.mrt_extra_factorization_energy line 31