Theorem 10.3 — Eventual scaled upper bound

Open

Erdos390.eventual_scaled_upper_bound

by ShouqiaoWang · Jul 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptoticscombinatoricserdos-problemsnumber-theoryupper-bound

Let $f(n)$ be the least possible largest factor in a representation of $n!$ as a product of distinct integers all greater than $n$ , and let

C_0=\frac{4029639598}{25970038185}.

For every real constant $c>C_0$ , all sufficiently large natural numbers $n$ satisfy

f(n)\le 2n+\left\lceil c\frac{n}{\log n}\right\rceil.

This is the paper's eventual upper-bound construction expressed directly as an endpoint estimate.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

/-- The paper's eventual upper endpoint for every constant above `C0`. -/
theorem eventual_scaled_upper_bound :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        f n ≤ 2 * n + Nat.ceil (c * secondOrderScale n) := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 103, Section 10, Theorem 10.3 (Upper-bound construction), https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L10062-L10179. Exact expanded formal endpoint statement: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSectionNinePostHeightSourceFirstMainAsymptoticConnectorStatementAudit.lean#L31-L53.

View graph