Skip to content

Erdős problem 1085

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

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1085.lean

Retained formal statement7 of 7

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.

FormalConjectures/ErdosProblems/1085.leanErdos1085.erdos_1085.variants.upper_lower_d5_odd8 linesExact file
∀ {d : ℕ},  5 ≤ d →    Odd d →      ∃ c₁ > 0,        ∃ c₂,          ∀ᶠ (n : ℕ) in Filter.atTop,            ↑(d / 2 - 1) / (2 * ↑(d / 2)) * ↑n ^ 2 + c₁ * ↑n ^ (4 / 3) ≤ ↑(Erdos1085.f d n) ∧              ↑(Erdos1085.f d n) ≤ ↑(d / 2 - 1) / ↑(d / 2) * ↑n ^ 2 + c₂ * ↑n ^ (4 / 3)
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page