claimroutineinferred_dep

Marginal atom lower bounds by vertex removal

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

Statement (paper)

For all sufficiently large

t

, every

p\in P

and

q\in Q

satisfy

\mu(p)\ge\gamma/|P|

and

\kappa(q)\ge\gamma/|Q|

, where

\gamma=27/50

; that is, holds, and multiplying by

|E|

gives the corresponding lower bounds on the degrees

d(p)

and

d(q)

in .

In plain English

For all large

t

, every

p\in P

and

q\in Q

has marginal mass

\mu(p)\ge\gamma/|P|

and

\kappa(q)\ge\gamma/|Q|

with

\gamma=27/50

. Equivalently, after multiplying by

|E|

, every degree

d(p)

and

d(q)

meets the corresponding lower bound.

Why it's here

This gives the vertex-wise lower bounds on marginals, which are the atom condition in the proposition. The likely route is vertex removal: compare the density-maximizing rectangle from the previous claim with the rectangle that omits a single low-degree vertex. Since that rectangle keeps a

t^{-o(a)}

fraction of the vertices and edges, a vertex with too small a marginal could be removed to raise the ratio

w/(uv)^\gamma

, contradicting maximality.

Classified routine:

A standard vertex-removal argument applied to the density-maximizing rectangle of claim-inc-piece-5. If some vertex had marginal below gamma/|P|, deleting it would increase the ratio w/(uv)^gamma, contradicting maximality; this is the usual technique for obtaining a minimum-degree subgraph.

Uses

claimDensity-maximizing rectangle retains large fractions

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Marginal atom lower bounds by vertex removal" rests on claim-inc-piece-5