IntermediateBandDecay.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.eventually_affine_loglog_le_log line 12
Source documentation
A fixed affine function of the iterated logarithm is negligible beside any positive multiple of the logarithm.
```
theorem eventually_affine_loglog_le_log (A B c : ℝ) (hc : 0 < c) :
    ∀ᶠ S : ℝ in atTop, A + B * Real.log (Real.log S) ≤ c * Real.log S := by
…
```

theorem OAI.Problem337.eventually_intermediate_band_envelope line 29

Source documentation

Uniform analytic domination for the intermediate-prime band. The conditions on B, Q, and the logarithmic factor are the coarse bounds obtained from the manuscript's ranges for v and t.

theorem eventually_intermediate_band_envelope
    (r C E : ℝ) (hr : 0 ≤ r) (hC : 0 ≤ C) (hE : 0 < E) :
    ∀ᶠ S : ℝ in atTop, ∀ B Q L : ℝ,
      B ≤ 1 + Real.log (2 * E * Real.log S) →
      S ^ (1 / 32 : ℝ) ≤ Q → L ≤ 2 * Real.log S →
      r * B * Q - Q * Real.log Q / 50 + C * Q ^ (1 / 5 : ℝ) * L ≤
        -(Q * Real.log Q) / 100 := by
…

theorem OAI.Problem337.eventually_rpow_half_le_log_range line 85
Source documentation
The lower endpoint in the divisor-moment range eventually exceeds the square root of the main parameter.
```
theorem eventually_rpow_half_le_log_range :
    ∀ᶠ S : ℝ in atTop, S ^ (1 / 2 : ℝ) ≤ S / (2 * Real.log S) := by
…
```

theorem OAI.Problem337.eventually_divisor_intermediate_band_decay line 107

Source documentation

The exact uniform intermediate-band estimate from the divisor-moment argument. Constants remain fixed while S, v, and t vary.

theorem eventually_divisor_intermediate_band_decay
    (D r C : ℝ) (hD : 1 ≤ D) (hr : 0 ≤ r) (hC : 0 ≤ C) :
    ∀ᶠ S : ℝ in atTop, ∀ v t : ℝ,
      S / (2 * Real.log S) ≤ v → v ≤ D * S →
      4 * Real.log S ≤ t → t ≤ v ^ (15 / 16 : ℝ) →
      r * (1 + Real.log ((D + 1) * 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.D, OAI.Problem337.v

theorem OAI.Problem337.eventually_affine_log_le_rpow line 163

Source documentation

Fixed affine logarithmic functions are dominated by any positive power.

theorem eventually_affine_log_le_rpow (A B δ a : ℝ)
    (hδ : 0 < δ) (ha : 0 < a) :
    ∀ᶠ S : ℝ in atTop, A + B * Real.log S ≤ δ * S ^ a := by
…

theorem OAI.Problem337.eventually_rpow_le_log_range line 177
Source documentation
Every fixed sublinear power lies below the divisor-moment lower range.
```
theorem eventually_rpow_le_log_range (a : ℝ) (ha : a < 1) :
    ∀ᶠ S : ℝ in atTop, S ^ a ≤ S / (2 * Real.log S) := by
…
```

theorem OAI.Problem337.eventually_divisor_small_prime_absorption line 195

Source documentation

The pointwise divisor bound and smooth-prefix Euler-product loss are uniformly negligible compared with the negative small-prime Rankin exponent.

theorem eventually_divisor_small_prime_absorption
    (E r C : ℝ) (hE : 0 < E) (hr : 0 ≤ r) (_hC : 0 ≤ C) :
    ∀ᶠ S : ℝ in atTop, ∀ v : ℝ,
      S / (2 * Real.log S) ≤ v →
      C * S ^ (2 / 5 : ℝ) +
        r * (S ^ (1 / 2 : ℝ) * Real.log (1 + E * S / Real.log 2) +
          2 * (1 + Real.log (E * S / v)) * v / Real.log S) ≤ v / 100 := by
…

Mentions: OAI.Problem337.v

theorem OAI.Problem337.eventually_uniform_in_log_range line 273
Source documentation
An eventual estimate in v holds uniformly throughout the logarithmic lower range of the divisor-moment lemma.
```
theorem eventually_uniform_in_log_range {P : ℝ → Prop}
    (hP : ∀ᶠ v : ℝ in atTop, P v) :
    ∀ᶠ S : ℝ in atTop, ∀ v : ℝ, S / (2 * Real.log S) ≤ v → P v := by
…
```
Mentions: OAI.Problem337.v
theorem OAI.Problem337.eventually_divisor_prefix_gap line 286
Source documentation
Uniform form of the positive logarithmic prefix gap used in both small- and intermediate-prime ranges.
```
theorem eventually_divisor_prefix_gap :
    ∀ᶠ S : ℝ in atTop, ∀ v : ℝ, S / (2 * Real.log S) ≤ v →
      v / 5 < v / 4 - v ^ (15 / 16 : ℝ) := by
…
```
Mentions: OAI.Problem337.v

theorem OAI.Problem337.eventually_divisor_band_rankin_parameter line 303

Source documentation

The Rankin exponent chosen in each intermediate band stays in the uniform interval required by the Euler local-factor estimate.

theorem eventually_divisor_band_rankin_parameter (D : ℝ) (_hD : 1 ≤ D) :
    ∀ᶠ S : ℝ in atTop, ∀ v t : ℝ,
      S / (2 * Real.log S) ≤ v → v ≤ D * S →
      4 * Real.log S ≤ t → t ≤ v ^ (15 / 16 : ℝ) →
      0 < Real.log (v / t) / (10 * t) ∧
        Real.log (v / t) / (10 * t) < 1 / 4 := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.v

theorem OAI.Problem337.eventually_small_rankin_exponent_le line 342
Source documentation
Direct interface for combining the small-prime smooth tail with an arbitrarily small pointwise divisor exponent.
```
theorem eventually_small_rankin_exponent_le (C : ℝ) :
    ∀ᶠ S : ℝ in atTop, ∀ v R : ℝ,
      S / (2 * Real.log S) ≤ v → R ≤ v / 200 →
      -v / 50 + C * S ^ (2 / 5 : ℝ) + R ≤ -v / 100 := by
…
```
Mentions: OAI.Problem337.v