OAI/Analysis/CircleDomains/Sobolev/CurveCoareaInput.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The plane-to-line specialization of Esmayli–Hajłasz, The Coarea Inequality, Ann. Fenn. Math. 46 (2021), 965–991, Theorem 1.1, DOI 10.5186/aasfm.2021.4654. The authors' manuscript is https://arxiv.org/pdf/2006.00419 (Theorem 1.1, p. 1; proof, §7).

Only s=t=1, X=ℂ and Y=ℝ is retained. The Hausdorff normalization constant is one in these dimensions. The source's measurability clause requires finite H¹ measure and a measurable set in a boundedly compact space; all these hypotheses are retained.

  1. def OAI.CircleDomainRigidity.PlanarLipschitzFiberCoarea line 22
  2. theorem OAI.CircleDomainRigidity.cardinalitySum_le_hausdorffZero line 29
  3. theorem OAI.CircleDomainRigidity.pathImageCount_le_hausdorffZero line 43
  4. theorem OAI.CircleDomainRigidity.integrated_pathImageCount_le_length line 48