Prove2Me

Level cap, general form: log ratio bounded by level exponent

Proved
gpy_log_ratio_lt_of_level

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theory

A level constraint R^2 < Y'^(theta - eta) with Y' > 1 caps the sieve log ratio log R / log Y' at theta/2 - eta/2. Pure Mathlib statement.

Preamble
import Mathlib
open Classical
Formal statement
theorem gpy_log_ratio_lt_of_level {R Y' : ℕ} {θ η : ℝ}
    (hR : 2 ≤ R) (hY : 1 < Y')
    (hlev : (R : ℝ) ^ 2 < (Y' : ℝ) ^ (θ - η)) :
    Real.log (R : ℝ) / Real.log (Y' : ℝ) < θ / 2 - η / 2 := by sorry
Source
GPY ratio analysis: threshold, main-term approximations, and BV level cap

View graph