Erdős problem 92

A sanity check to ensure the set of possible `f(n)` values is bounded above. A trivial bound is `n`, since the points equidistant from any `x` form a subset of the other `n - 1` points. This ensures `sSup` is well-defined.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

92.lean

Retained formal statement1 of 3

Or even $f(n) < n^{c/\log\log n}$ for some constant $c > 0$ ?

FormalConjectures/ErdosProblems/92.leanErdos92.erdos_92.variants.strong1 lineExact file

1sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))

OpenStatement only, no proof