Prove2Me

Quantitative bounds imply exponent 1/21/2

Proved
Erdos788.quantitativeMainTheorem_implies_hasExponentOneHalf

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

asymptoticscombinatoricserdos-problemsexponent

Assume there are constants c,C>0c,C>0 and a threshold n0≥1n_0\ge1 for which every n≥n0n\ge n_0 satisfies

cnlog⁡n≤f(n)≤n 12+C(log⁡log⁡nlog⁡n)1/3.c\sqrt{n\log n}\le f(n)\le n^{\,\frac12+ C\left(\frac{\log\log n}{\log n}\right)^{1/3}}.

Then ff has exponent one-half in the fully quantified sense: for every ε>0\varepsilon>0, there is Nε≥1N_\varepsilon\ge1 such that every n≥Nεn\ge N_\varepsilon obeys

n1/2−ε≤f(n)≤n1/2+ε.n^{1/2-\varepsilon}\le f(n)\le n^{1/2+\varepsilon}.

This theorem isolates the exact logical passage from the quantitative estimate to the n1/2+o(1)n^{1/2+o(1)} formulation.

Preamble
import Definitions.Def_erdos788_problem
Formal statement
namespace Erdos788

/-- The quantitative two-sided theorem implies the full epsilon formulation
of exponent one half. -/
theorem quantitativeMainTheorem_implies_hasExponentOneHalf
    (hmain : QuantitativeMainTheorem) :
    HasExponentOneHalf := by sorry

end Erdos788
Source
Shouqiao Wang, Erdős Problem 788 formalization, ExponentConsequences.lean, lines 13–81: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/lean/Erdos788/ExponentConsequences.lean#L13-L81. Reference manuscript: https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/788/paper.pdf, consequence of Theorem 1.1.

View graph