DivisorBandDecay.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.DivisorMoment.tendsto_loglog_coefficient line 12
Source documentation
The slowly varying coefficient in the prime-prefix band estimate is negligible compared with the logarithm of the band parameter.
```
theorem tendsto_loglog_coefficient (r K : ℝ) :
    Tendsto (fun v : ℝ => r * (K + Real.log (Real.log v)) / Real.log v)
      atTop (𝓝 0) := by
…
```
Mentions: OAI.Problem337.v

theorem OAI.Problem337.DivisorMoment.eventually_intermediate_band_decay line 26

Source documentation

Uniform domination of the two positive errors in an intermediate-prime band.

theorem eventually_intermediate_band_decay (r C K : ℝ) (hr : 0 ≤ r) (hC : 0 ≤ C) :
    ∀ᶠ v : ℝ in atTop, ∀ Q t B : ℝ,
      v ^ (1 / 16 : ℝ) ≤ Q → 0 < t → t ≤ v →
      B ≤ K + Real.log (Real.log v) →
      r * B * Q - Q * Real.log Q / 50 +
        C * Q ^ (1 / 5 : ℝ) * Real.log (2 * t) ≤ -Q * Real.log Q / 100 := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.DivisorMoment.eventually_uniform_intermediate_band_decay line 80

Source documentation

The intermediate-prime exponent is uniformly negative over all admissible logarithmic scales. Only the lower bound on v is needed.

theorem eventually_uniform_intermediate_band_decay (E r C : ℝ)
    (hE : 2 ≤ E) (hr : 0 ≤ r) (hC : 0 ≤ C) :
    ∀ᶠ S : ℝ in atTop, ∀ v t : ℝ,
      S / (2 * Real.log S) ≤ v → 0 < t → t ≤ v ^ (15 / 16 : ℝ) →
      r * (1 + Real.log (E * S / v)) * (v / t) -
        (v / t) * Real.log (v / t) / 50 +
        C * (v / t) ^ (1 / 5 : ℝ) * Real.log (2 * t) ≤
          -(v / t) * Real.log (v / t) / 100 := by
…

Mentions: OAI.Problem337.v