OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRamareWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Positive coefficient weights in the uncorrected Ramaré polynomial. They have total mass at most one, even at integers divisible by prime squares. This is the contraction needed for logarithmic-bin cutoffs.

  1. def OAI.TwoPointCorrelations.mrtRamareWeight line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareWeights.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrtRamareWeight_nonneg line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareWeights.lean:17 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_ramare_weight_le_count line 22

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareWeights.lean:22 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_ramare_weight_sum_le_one line 35

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareWeights.lean:35 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.mrt_ramare_weighted_contraction line 61

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRamareWeights.lean:61 (same declaration text).