OAI/Analysis/CircleDomains/Sobolev/SmoothCurveCoarea.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Differential-weighted curve coarea, derived from the published constant-Lipschitz inequality by a disjoint local cover. No new coarea input is assumed.

  1. theorem OAI.CircleDomainRigidity.curve_coarea_lipschitzOn line 18
  2. theorem OAI.CircleDomainRigidity.smooth_curve_coarea_add_error line 32
  3. theorem OAI.CircleDomainRigidity.smooth_curve_coarea_bound line 79