Proof of Lemma 3, p. 14 — f(q) = LU/q + q bounds the objective of (5) below, f(L) = f(U) = L + U, and f is minimized at √(LU)

Proved

JRPHard.RangeDiv.f_at_L_U

by mikedeng1 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

am-gmgcdp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1range-divisor

Let $M \ge U \ge L > 0$ be integers with $L + U < 2\sqrt{2LU}$ , and let $f(x) = LU/x + x$ for real $x > 0$ . Then:

for every positive integer $q$ , $f(q) \le \dfrac{LU}{\gcd(q,M)} + q$ ;
$f(L) = f(U) = L + U$ ;
$f$ is minimized at $\sqrt{LU}$ : for every real $x > 0$ ,

f\big(\sqrt{LU}\big) \le f(x).

The function $f$ coincides with the objective of problem (5) at divisors of $M$ and lies below it everywhere. It meets the level $L + U$ exactly at the two ends of the interval $[L, U]$ .

Preamble

import Mathlib
import Definitions.Def_JRPHard_RangeDiv_Setting

Formal statement

namespace JRPHard.RangeDiv

theorem f_at_L_U (M L U : ℕ) (hI : IsRangeDivisorInstance M L U) :
    (∀ q : ℕ, 0 < q → fConv L U q ≤ obj5 M L U q) ∧
    fConv L U L = L + U ∧ fConv L U U = L + U ∧
    (∀ x : ℝ, 0 < x → fConv L U (Real.sqrt ((L : ℝ) * U)) ≤ fConv L U x) := by sorry

end JRPHard.RangeDiv

Source

Schulz and Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, p. 14, §3.1, proof of Lemma 3, "The convex function f(q) ≡ K₀/q + q"

Human review

Endorsed by Shuze Chen · Oct 15, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph