claimroutine

Cutting deletion loses few incidences

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

Statement (paper)

With R=t1−aR=t^{1-a} and s=O(t1−alog⁡t)s=O(t^{1-a}\log t) in , the incidences lost by the deletion (those on the sampled circles, at most st3st^3, together with those at deleted points with other circles, at most 2st32st^3) number O(t4−alog⁡t)=o(t4−o(a))O(t^{4-a}\log t)=o(t^{4-o(a)}), so the remaining incidence count is still at least t4−o(a)t^{4-o(a)}.

In plain English

With R=t1−aR=t^{1-a} and s=O(t1−alog⁡t)s=O(t^{1-a}\log t) in the cutting lemma, the points deleted (those on sampled circles, plus the others) destroy only O(t4−alog⁡t)=o(t4−o(a))O(t^{4-a}\log t)=o(t^{4-o(a)}) incidences, so at least t4−o(a)t^{4-o(a)} incidences remain.

Why it's here

The deletion step in the cutting lemma could in principle wipe out the incidence supply, so this claim checks that it does not: the lost count O(st3)O(st^3) is smaller than t4−o(a)t^{4-o(a)} by a factor of about tat^{a}. This lets the next claim apply the region and piece decomposition to a point set that still carries essentially all the incidences.
Classified routine:
Direct bookkeeping from the random-sampling cutting lemma (inc-cutting): with these parameter choices the lost incidences are at most O(st^3), which is smaller than the incidence count by a factor of about t^a.

Uses

lemUnit distances persist under algebraic perturbationlemRandom-sampling cutting for unit circles

Used by

claimSome small piece carries many incidences

Sources

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

Phase 2 aligns this node to a Lean declaration.