claimroutineinferred_dep

Preliminary square-root expansion bound

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

Statement (paper)

For subsets of the trimmed vertex sets

(P_0,Q_0)

with counting fractions

u,v

and captured edge fraction

w

, there is a factor

T_t=t^{o(a)}

, uniform over all such subsets, such that

w\le T_t\sqrt{uv}\bigl((uv)^{1/6}+2t^{-a/2}\bigr)

In plain English

For any subsets of the trimmed vertex sets

(P_0,Q_0)

with counting fractions

u,v

and captured edge fraction

w

, we have

w\le T_t\sqrt{uv}\bigl((uv)^{1/6}+2t^{-a/2}\bigr)

for a factor

T_t=t^{o(a)}

that is uniform over all such subsets.

Why it's here

This is a first expansion estimate on the trimmed graph. It combines the degree bounds from the trimming claim with the Szemerédi–Trotter bound for unit circles, which gives the

\sqrt{uv}

decay with a weak exponent

1/6

and a small additive term. The next claims use it to show a density-maximizing rectangle cannot be too small, and then to sharpen the exponent to

\eta

Classified routine:

Direct consequence of the Szemerédi–Trotter incidence bound for unit circles (Spencer–Szemerédi–Trotter 1984) combined with the degree bounds from the preceding trimming claim; the (uv)^{1/6} term and the additive term come from the m^{2/3}l^{2/3} and linear terms after normalizing.

Uses

claimTrimming high-degree vertices gives degree boundspropSzemerédi–Trotter bound for unit circles

Used by

claimDensity-maximizing rectangle retains large fractionsclaimSharpened expansion bound from maximality

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Preliminary square-root expansion bound" rests on claim-inc-piece-3
info
inferred_dep
outline: "Preliminary square-root expansion bound" rests on inc:incidence