OAI/Analysis/CircleDomains/Sobolev/PhysicalLipschitzCoarea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact weighted coarea for a Lipschitz function on the physical Euclidean plane, with the norm of its actual differential.

  1. def OAI.CircleDomainRigidity.PhysicalWeightedCoareaIdentity line 13
  2. lemma OAI.CircleDomainRigidity.physical_lipschitz_weighted_coarea line 19