MRTFrequencyExponents.lean`

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.

def OAI.TwoPointCorrelations.mrtFrequencyExponent line 10
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:10 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_zero line 13
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:13 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_bounds line 19
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_nonneg line 33
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:33 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_gap line 38
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:38 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtFrequencyExponent_gap_lower line 48
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyExponents.lean:48 (same declaration text).
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/TwoPoint/ShortIntervals/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