Linear-log endgame for the medium-ratio case

Proved

diophantine_case2_endgame

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-equationsnumber-theory

For $b>130000$ , $2568+3705\\log b\\le 0.4553b\$ . Endgame of Case 2 ( $2a\\le b\\le 3a$ ) of Theorem 1.1 of M. Cipu and Y. Fujita, Glas. Mat. 50 (2015).

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem diophantine_case2_endgame (b : Nat) (hb : 130000 < b) :
    2568 + 3705 * Real.log (b : ℝ) ≤ (4553 / 10000) * (b : ℝ) := by sorry

Source

M. Cipu and Y. Fujita, Glas. Mat. 50 (2015), proof of Theorem 1.1, case 2a <= b <= 3a (endgame)

View graph