OAI/Analysis/CircleDomains/Selection/ChordTolls.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Accounting for chord tolls

The temporary chord enumeration carries the costs of its actual disks. Summing over that enumeration charges exactly the disks meeting the segment, and hence at most all disks meeting the whole parallel line.

  1. def OAI.CircleDomainRigidity.chordToll line 17
  2. theorem OAI.CircleDomainRigidity.le_chordToll line 23
  3. theorem OAI.CircleDomainRigidity.sum_chordToll line 34
  4. theorem OAI.CircleDomainRigidity.sum_chordToll_le_line_hits line 47