OAI/Analysis/CircleDomains/Modulus/DiskLinePayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Variation across the round holes met by one line

This derives the linewise payment directly from smoothness on the complement of the actual disks and their cluster oscillations. No endpoint extension or pre-existing line-payment hypothesis is assumed.

  1. def OAI.CircleDomainRigidity.diskLineDomain line 20
  2. theorem OAI.CircleDomainRigidity.isOpen_diskLineDomain line 23
  3. theorem OAI.CircleDomainRigidity.line_payment_through_disks line 29