OAI/NumberTheory/TwoPointCorrelations/MRTCofactorMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The mixed moment needed by the second and later MRT frequency classes. This is the actual reciprocal-count cofactor, with arbitrary one-bounded remaining masks. Its only loss is the explicit prime-tuple factorial.

  1. theorem OAI.TwoPointCorrelations.mrt_short_prime_cofactor_moment line 16

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCofactorMoment.lean:16 (same declaration text).