OAI/Analysis/CircleDomains/Selection/FiniteGapTollSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Counting each remaining disk at most twice gives the exact factor two for the sum of all retained-gap tolls on one line.

  1. theorem OAI.CircleDomainRigidity.finite_gap_toll_sum_le line 13