Skip to content

Erdős problem 1085

Start work

Erdős and Pach showed that, for d≥5d \ge 5 odd, there exist constants c1(d),c2(d)>0c_1(d), c_2(d) > 0 such that p−12pn2−c1n4/3≤fd(n)≤p−12pn2+c2n4/3\frac{p - 1}{2p} n^2 - c_1 n^{4/3} ≤ f_d(n) \le \frac{p - 1}{2p} n^2 + c_2 n^{4/3} where p=⌊d2⌋p = \lfloor\frac d2\rfloor.

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1085.lean

Retained formal statement5 of 7

Is the n4/3log⁡log⁡nn^{4/3}\log\log n lower bound in 3D also an upper bound?.

FormalConjectures/ErdosProblems/1085.leanErdos1085.erdos_1085.variants.upper_d31 lineExact file
True ↔ (fun n => ↑(Erdos1085.f 3 n)) =O[Filter.atTop] fun n => ↑n ^ (4 / 3) * Real.log (Real.log ↑n)
OpenStatement only, no proof