Superlinear convex unit-distance family
OpenErdos9796Mission.problem96_superlinear_familyconvex-positiondiscrete-geometryerdos-96unit-distances
For every nonnegative proposed linear constant and every cutoff, some larger cardinality has maximum convex unit-distance count exceeding that constant times the cardinality.
Preamble
import Definitions.Def_Erdos9796Mission
Formal statement
theorem Erdos9796Mission.problem96_superlinear_family :
∀ C : ℝ, 0 ≤ C → ∀ N : ℕ, ∃ n : ℕ,
N ≤ n ∧
C * (n : ℝ) <
(Erdos9796Mission.maxConvexUnitDistances n : ℝ) := by sorrySource