OAI/Analysis/CircleDomains/Rigidity/RemovableAreaZero.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A compact removable set in the finite chart has zero planar area. A principal real Beltrami solution with conductivity two on that set must be the identity. Uniqueness of its weak derivatives then forces the set to be null. Only the already recorded principal Beltrami input is used.

  1. theorem OAI.CircleDomainRigidity.weak_coordinate_one line 17
  2. theorem OAI.CircleDomainRigidity.removable_physical_compact_volume_zero line 32
  3. theorem OAI.CircleDomainRigidity.removable_complement_volume_zero line 89