claimroutineinferred_dep

Sharpened expansion bound from maximality

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

Statement (paper)

For every F⊆PF\subseteq P and G⊆QG\subseteq Q, with counting fractions u=∣F∣/∣P∣u=|F|/|P| and v=∣G∣/∣Q∣v=|G|/|Q|, one has PE(p∈F,q∈G)≤uv((uv)η+ξt)\Prob_E(p\in F,q\in G)\le \sqrt{uv}\bigl((uv)^\eta+\xi_t\bigr), where ξt=t−a/48+o(a)→0\xi_t=t^{-a/48+o(a)}\to0 is independent of the chosen subsets. For feasible subsets (Uu,Vv≥τUu,Vv\ge\tau) optimality gives PE(F,G)≤(uv)γ\Prob_E(F,G)\le(uv)^\gamma, and for infeasible subsets PE(F,G)≤to(a)uv((uv)1/6+2t−a/2)≤ξtuv\Prob_E(F,G)\le t^{o(a)}\sqrt{uv}\bigl((uv)^{1/6}+2t^{-a/2}\bigr)\le\xi_t\sqrt{uv} uniformly.

In plain English

For all F⊆PF\subseteq P and G⊆QG\subseteq Q with fractions u,vu,v, PE(p∈F,q∈G)≤uv((uv)η+ξt)\Prob_E(p\in F,q\in G)\le\sqrt{uv}\bigl((uv)^\eta+\xi_t\bigr), where ξt=t−a/48+o(a)→0\xi_t=t^{-a/48+o(a)}\to0 does not depend on the subsets.

Why it's here

This is the final expansion estimate in the proposition, obtained by splitting into two cases. Feasible subsets (Uu,Vv≥τUu,Vv\ge\tau) are controlled by the density-maximizing rectangle, which gives (uv)γ=uv(uv)η(uv)^\gamma=\sqrt{uv}(uv)^\eta. Infeasible subsets are small enough that the preliminary square-root bound already gives the ξtuv\xi_t\sqrt{uv} error term, uniformly in the subsets.
Classified routine:
A case split that follows directly from the earlier claims. Feasible subsets are bounded by the maximality of the density-maximizing rectangle (claim-inc-piece-5), and infeasible ones by the preliminary square-root expansion bound (claim-inc-piece-4) plus bookkeeping of the exponents.

Uses

claimPreliminary square-root expansion boundclaimDensity-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:303
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Expansion estimate from optimality of rectangle" rests on claim-inc-piece-4
  • info
    inferred_dep
    outline: "Expansion estimate from optimality of rectangle" rests on claim-inc-piece-5