OAI/NumberTheory/TwoPointCorrelations/MRTWeightedTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Partial summation of the supported-divisor second moment. This keeps the mixed Dirichlet coefficient square mass proportional to the inverse lower endpoint, rather than losing the ratio of its endpoints.

  1. lemma OAI.TwoPointCorrelations.mrt_real_prefix_zero_extension line 15

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWeightedTail.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_square_reciprocal_partial_sum line 25

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWeightedTail.lean:25 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_weighted_square_tail line 53

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWeightedTail.lean:53 (same declaration text).