Section 3, inequality (1) — $.6x_1 + (1-x_1)^{2/3} > 1$ has no solution in $0 < x_1 \le 1/2$

Proved

SzemerediTrotter.Incidence.inequality_1_no_solution

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

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

For every real number $x$ with $0 < x \le \tfrac12$ ,

0.6\,x + (1-x)^{2/3} \le 1.

Equivalently, inequality (1) of Szemerédi and Trotter, $0.6\,x_1 + (1-x_1)^{2/3} > 1$ , has no solution in the range $0 < x_1 \le 1/2$ . In the proof of Theorem 1 this rules out a positive fraction of lines of low density (and, by the same argument, of points of low degree) in a minimal counterexample.

Formalization Note The power $(1-x)^{2/3}$ is the real power Real.rpow with exponent the real number $2/3$ ; on the stated range the base $1-x$ is in $[1/2, 1)$ , so no convention for negative bases is involved.

Preamble

import Mathlib

Formal statement

namespace SzemerediTrotter.Incidence

/-- Section 3, inequality (1), p. 384: `.6x₁ + (1 − x₁)^{2/3} > 1` has no solution with
`0 < x₁ ≤ 1/2`. -/
theorem inequality_1_no_solution :
    ∀ x : ℝ, 0 < x → x ≤ 1 / 2 → (0.6 : ℝ) * x + (1 - x) ^ (2 / 3 : ℝ) ≤ 1 := by sorry

end SzemerediTrotter.Incidence

Source

Szemerédi, Trotter, Extremal Problems in Discrete Geometry, Combinatorica 3 (1983), p. 384, Section 3, inequality (1)

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

Section 3, inequality (1) — .6x1+(1−x1)2/3>1.6x_1 + (1-x_1)^{2/3} > 1.6x1​+(1−x1​)2/3>1 has no solution in 0<x1≤1/20 < x_1 \le 1/20<x1​≤1/2

Section 3, inequality (1) — $.6x_1 + (1-x_1)^{2/3} > 1$ has no solution in $0 < x_1 \le 1/2$