OAI/Analysis/CircleDomains/Topology/RoundDiskGreen.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The existing signed Green input specializes to the positively parametrized round disk. Its sign is determined by the radial one-form, whose boundary integral and area integral are computed here.

  1. theorem OAI.CircleDomainRigidity.radial_form_unitCircleParam line 15
  2. theorem OAI.CircleDomainRigidity.round_disk_green line 31