OAI/Analysis/CircleDomains/Topology/ParallelDiskTolls.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact costs of round holes on parallel lines

The horizontal lines meeting a closed round disk form an interval of length twice its radius. Integrating finitely many hole tolls therefore gives exactly the radius-weighted sum. Disjointness and a common containing disk bound this sum by the square norm of the oscillation tolls.

  1. theorem OAI.CircleDomainRigidity.horizontal_line_meets_closedBall line 19
  2. theorem OAI.CircleDomainRigidity.integral_parallel_disk_tolls line 36
  3. theorem OAI.CircleDomainRigidity.real_volume_closedBall line 51
  4. theorem OAI.CircleDomainRigidity.sum_radii_sq_le_of_disjoint_closed_disks line 55
  5. theorem OAI.CircleDomainRigidity.parallel_disk_tolls_le_square_norm line 70