Erdős problem 1085 · problems.science

Erdős and Pach showed that, for $d \ge 5$ odd, there exist constants $c_1(d), c_2(d) > 0$ such that $\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 = \lfloor\frac d2\rfloor$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1085.lean

Retained formal statement6 of 7

Erdős showed that, for $d \ge 4$ , $f_d(n) \le \left(\frac{p - 1}{2p} + o(1)\right) n^2$ where $p = \lfloor\frac d2\rfloor$ .

FormalConjectures/ErdosProblems/1085.leanErdos1085.erdos_1085.variants.upper_d4_erdos5 linesExact file

1∀ {d : ℕ},2  4 ≤ d →3    ∃ g,4      Filter.Tendsto g Filter.atTop (nhds 0) ∧5        ∀ (n : ℕ), ↑(Erdos1085.f d n) ≤ (↑(d / 2 - 1) / (2 * ↑(d / 2)) + g n) * ↑n ^ 2

SolvedStatement only, no proof

Sources

Search problems.science