OAI/Analysis/CircleDomains/Rigidity/CountableAxialDiskTolls.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Countable axial disk tolls are integrable with their exact mixed-radius budget. Point disks are missed outside a countable set of lines.

  1. theorem OAI.CircleDomainRigidity.complexCoordinateLine_meets_closedBall line 14
  2. def OAI.CircleDomainRigidity.axialDiskToll line 35
  3. theorem OAI.CircleDomainRigidity.axialDiskToll_integrable line 39
  4. theorem OAI.CircleDomainRigidity.axial_point_disk_lines_null line 64