OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWorkingBand.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.mrt_working_upper_log line 12
2. lemma OAI.TwoPointCorrelations.mrt_working_band_budget line 34
3. lemma OAI.TwoPointCorrelations.mrt_working_band_resolution line 47
4. lemma OAI.TwoPointCorrelations.mrt_working_band_density line 67

   Source documentation

   The density cost is bounded by the original logarithmic length term or, on the capped branch, by W^(-1/4).

   lemma mrt_working_band_density (A : ℕ) {H : ℕ} {W : ℝ}
       (hW : 2 ≤ W) (hLH : 1 ≤ Real.log (H : ℝ))
       (hWH : W ≤ (Real.log (H : ℝ)) ^ (5 : ℕ))
       (hpower : W ^ (6 : ℕ) ≤ (mrtWorkingLength H W : ℝ))
       (hcap : Real.sqrt W / 4 ≤ Real.log (mrtWorkingCap W : ℝ))
       (hsmall : Real.log W ≤ W ^ (1 / 4 : ℝ)) :
       Real.log (W ^ A) / Real.log ((mrtWorkingLength H W : ℝ) / W ^ (3 : ℕ)) ≤
         10 * (A : ℝ) * (Real.log (Real.log (H : ℝ)) / Real.log H +
           W ^ (-(1 / 4 : ℝ))) := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtWorkingLength, OAI.TwoPointCorrelations.mrtWorkingCap