Prove2Me

Section 3, inequality (5) — no solution in (0,.1](0,.1], a solution in (.1,.2)(.1,.2)

Proved
SzemerediTrotter.Incidence.inequality_5_no_solution

by mikedeng1 · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1real-inequalities

Consider the function

f(x)=x2/3+1−x100+2−1/3(1−x)2/3.f(x) = x^{2/3} + \frac{1-x}{100} + 2^{-1/3}(1-x)^{2/3}.
  1. For every real xx with 0<x≤0.10 < x \le 0.1 one has f(x)≤1f(x) \le 1; that is, inequality (5) of Szemerédi and Trotter, 1<f(x0)1 < f(x_0), has no solution in the interval (0,0.1](0, 0.1].
  2. There is a real xx with 0.1<x<0.20.1 < x < 0.2 and 1<f(x)1 < f(x); that is, inequality (5) does have a solution in (0.1,0.2)(0.1, 0.2).

In the proof of Theorem 1 the first part shows that the set P0\mathcal P_0 of points incident with many lines from both halves of the slope-ordered family has at least a tenth of the points. The second part is the paper's parenthetical remark that the threshold 0.10.1 cannot be raised to 0.20.2 by this inequality alone.

Formalization Note All powers are Real.rpow with real exponents 2/32/3 and −1/3-1/3; on the stated ranges all bases are positive.

Preamble
import Mathlib
Formal statement
namespace SzemerediTrotter.Incidence

/-- Section 3, inequality (5), p. 385: `1 < x₀^{2/3} + (1 − x₀)/100 + 2^{−1/3}(1 − x₀)^{2/3}`
has no solution in `(0, .1]`, and it has a solution in `(.1, .2)`. -/
theorem inequality_5_no_solution :
    (∀ x : ℝ, 0 < x → x ≤ 0.1 →
      x ^ (2 / 3 : ℝ) + (1 - x) / 100 + (2 : ℝ) ^ (-(1 / 3) : ℝ) * (1 - x) ^ (2 / 3 : ℝ) ≤ 1) ∧
    (∃ x : ℝ, 0.1 < x ∧ x < 0.2 ∧
      1 < x ^ (2 / 3 : ℝ) + (1 - x) / 100 + (2 : ℝ) ^ (-(1 / 3) : ℝ) * (1 - x) ^ (2 / 3 : ℝ)) := by sorry

end SzemerediTrotter.Incidence
Source
Szemerédi, Trotter, Extremal Problems in Discrete Geometry, Combinatorica 3 (1983), p. 385, Section 3, inequality (5) and the sentence following it (printed as "inequality (2)", a misprint for (5))
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph