OAI/NumberTheory/TwoPointCorrelations/MRTMixedPolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact prime-power times cofactor polynomial identity. This attaches the proved mixed coefficient estimate to the actual expression used on the multiscale large-prime frequency classes.

  1. lemma OAI.TwoPointCorrelations.mrt_multiplicative_phase line 14

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedPolynomial.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_mixed_tuple_term line 24

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedPolynomial.lean:24 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_mixed_polynomial_identity line 39

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedPolynomial.lean:39 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_mixed_prime_cofactor_mean_square line 91

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedPolynomial.lean:91 (same declaration text).