OAI/Analysis/CircleDomains/Transfer/ComplexHausdorffTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The physical coordinate chart is an isometry, including for the Hausdorff-length measures on the full pointwise coarea levels.

  1. def OAI.CircleDomainRigidity.complexPlaneIsometry line 13
  2. theorem OAI.CircleDomainRigidity.complexPlaneCoordinates_hausdorff_preserving line 21
  3. theorem OAI.CircleDomainRigidity.complex_hausdorff_set_integral line 25
  4. theorem OAI.CircleDomainRigidity.complex_sobolev_level_integral line 31