OAI/Analysis/CircleDomains/Sobolev/LipschitzCoareaProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published plane-to-line coarea input, with its exact finite-H1 Borel-set hypotheses. Both the completed measurability and the sharp constant-one inequality are proved.

  1. lemma OAI.CircleDomainRigidity.planarLipschitzFiberCoarea line 15