OAI/Analysis/CircleDomains/Sobolev/LipschitzFiberIntegralBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The sharp one-dimensional coarea inequality from Hausdorff covers. No rectifiability is needed. Closed images of the covers are measurable majorants; Fatou's lemma passes their counting bounds to the fibers.

  1. lemma OAI.CircleDomainRigidity.lipschitz_fiber_integral_le line 16