Approximation bound for large numerators

Proved

OAI.PiExponent.rational_approximation_far_numerator_bound

by Eyal1990 · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

For every exponent nu greater than 2, denominator q at least 2, and integer numerator p with |p| greater than 4q, the desired lower bound holds.

Preamble

import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Formal statement

theorem OAI.PiExponent.rational_approximation_far_numerator_bound (nu : ℝ) (hnu : 2 < nu)
    (p : ℤ) (q : ℕ) (hq : 2 ≤ q) (hlarge : 4 * (q : ℝ) < |(p : ℝ)|) :
    (q : ℝ) ^ (-nu) ≤ |Real.pi - (p : ℝ) / (q : ℝ)| := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PiExponent.lean

View graph