claimroutineinferred_dep

Conflict bound via union over candidate regions

Claim·§2.2 Cuttings and the incidence bound·inside lemRandom-sampling cutting for unit circles

Statement (paper)

With probability at least 9/109/10, every open piece of the decomposition determined by the sampled circles intersects at most l/Rl/R of the original circles. This holds because there are at most C0(1+l)6C_0(1+l)^6 candidate regions, each described by a bounded number of circles from the full set, and for any fixed candidate region intersecting more than l/Rl/R circles the probability that no sampled circle intersects it is at most (1−1/R)s≤e−s/R(1-1/R)^s\le e^{-s/R}, so a union bound with CC sufficiently large gives failure probability at most 1/101/10.

In plain English

With probability at least 9/10, every open piece of the decomposition determined by the sampled circles meets at most l/Rl/R of the original circles. The proof union-bounds over at most C0(1+l)6C_0(1+l)^6 candidate regions, each described by boundedly many circles from the full set.

Why it's here

This is the conflict-bound step of the cutting lemma. A candidate region meeting more than l/Rl/R circles is missed by all ss samples with probability at most (1−1/R)s≤e−s/R(1-1/R)^s\le e^{-s/R}. Since s≈CRlog⁡(2+l)s\approx CR\log(2+l), a large enough CC makes the union bound over polynomially many candidates at most 1/101/10. Together with the sweep pieces from the previous claim, which avoid sampled circles and cover the remaining points, this shows the pieces are valid regions meeting at most l/Rl/R circles each.
Classified routine:
This is the standard random-sampling epsilon-net argument for cuttings (Clarkson–Shor style): a probability bound for each of polynomially many candidate regions, combined by a union bound. Here it is applied to unit circles.

Uses

claimSweep pieces avoid sampled circles and cover points

Used by

Nothing in the paper

Sources

PaperOpen
Section
§2.2 Cuttings and the incidence bound
Page
—
Label
—
Line
sections/01-incidence.tex:129
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Conflict bound via union over candidate regions" rests on claim-inc-cutting-2