OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The increasing prime-polynomial thresholds in MRT's multiscale partition, indexed from zero to match mrtFirstSmallBand.

  1. def OAI.TwoPointCorrelations.mrtFrequencyExponent line 10

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:10 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_zero line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:13 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_bounds line 19

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:19 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_nonneg line 33

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:33 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_gap line 38

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:38 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_gap_lower line 48

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyExponents.lean:48 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_frequency_gap_saving line 58

    Source documentation

    After paying half of the threshold gap for the mixed-moment factorial, the remaining exponential saving is still summable.

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

    lemma mrt_frequency_gap_saving {η x : ℝ} (hη : 0 ≤ η) (hx : 0 ≤ x) (j : ℕ) :
    2 * x * (mrtFrequencyExponent η j - mrtFrequencyExponent η (j + 1) +
      η / (4 * ((j : ℝ) + 2) ^ 2)) ≤ -η * x / (2 * ((j : ℝ) + 2) ^ 2) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtFrequencyExponent