OAI/Analysis/CircleDomains/Sobolev/PhysicalCoordinateCoarea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Apply weighted coarea to the actual smooth physical representative of a quotient coordinate.

  1. theorem OAI.CircleDomainRigidity.physicalRealCoordinate_ae_finite_weighted_levels line 20
  2. theorem OAI.CircleDomainRigidity.physicalRealCoordinate_ae_finite_level_length line 71