OAI/Analysis/CircleDomains/Modulus/FiniteCircleLinePayment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parallel-line payment on a finite circle domain

For a smooth real function on the complement of finitely many round disks, crossing segments pay through the actual Euclidean gradient and cluster oscillations. All endpoint traces and gap decompositions are constructed in the preceding modules.

  1. theorem OAI.CircleDomainRigidity.parallel_line_payment_on_finite_disk_complement line 22
  2. theorem OAI.CircleDomainRigidity.parallel_line_payment_on_finite_disk_complement_square_norm line 94