OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mean square of the actual mixed prime/cofactor coefficients. The factorial cost is explicit, while the finite Euler factor depends only on the preceding short prime band, not the number of typical-set masks.

  1. theorem OAI.TwoPointCorrelations.mrt_factored_coefficient_mass line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedMoment.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.mrt_mixed_coefficient_mean_square line 58

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedMoment.lean:58 (same declaration text).