claimroutineinferred_dep

Trimming high-degree vertices gives degree bounds

Claim·§2.3 Degree control and a maximizing rectangle·inside propIncidence piece with degree and expansion control

Statement (paper)

After deleting the point vertices of degree greater than

t^{1+b}

and the center vertices of degree greater than

t^{a+b}

, where

b=o(a)

and

b\log t\to\infty

, the trimmed graph

(P_0,Q_0,E_0)

retains

t^{2+2a+o(a)}

edges, has point degrees at most

t^{1+o(a)}

and center degrees at most

t^{a+o(a)}

, and both vertex sets attain their upper scales

|P_0|=t^{1+2a+o(a)}

and

|Q_0|=t^{2+a+o(a)}

within a factor

t^{o(a)}

In plain English

Deleting point vertices of degree above

t^{1+b}

and center vertices of degree above

t^{a+b}

(with

b=o(a)

b\log t\to\infty

) leaves a graph

(P_0,Q_0,E_0)

with

t^{2+2a+o(a)}

edges, point degrees at most

t^{1+o(a)}

, center degrees at most

t^{a+o(a)}

, and

|P_0|

|Q_0|

still at their upper scales

t^{1+2a}

and

t^{2+a}

up to a factor

t^{o(a)}

Why it's here

The previous claim gives a piece with about

t^{2+2a}

edges but no degree control. The edges at the deleted high-degree vertices are few, because the average degrees are about

t^{1}

for points and

t^{a}

for centers and the Szemerédi–Trotter edge cap bounds the totals, so most edges survive. The surviving edges, now with bounded degrees, force the vertex sets to be nearly as large as their upper bounds, which sets up the later expansion bounds on

(P_0,Q_0)

Classified routine:

A standard degree-trimming (dyadic pruning) argument. Szemerédi–Trotter caps the edges lost at high-degree vertices, and the vertex-set sizes follow by dividing the surviving edge count by the degree bounds. It applies inc-incidence to the piece supplied by claim-inc-piece-2.

Uses

claimSome small piece carries many incidencespropSzemerédi–Trotter bound for unit circles

Used by

claimPreliminary square-root expansion bound

Sources

PaperOpen

Section: §2.3 Degree control and a maximizing rectangle
Page: —
Label: —
Line: sections/01-incidence.tex:234

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Trimming high-degree vertices gives degree bounds" rests on claim-inc-piece-2
info
inferred_dep
outline: "Trimming high-degree vertices gives degree bounds" rests on inc:incidence