OAI/Analysis/CircleDomains/Sobolev/SobolevScalarCoarea.lean

The scalar planar specialization of Malý–Swanson–Ziemer, The co-area formula for Sobolev mappings, Trans. AMS 355 (2003), 477–492, Theorem 1.1, DOI 10.1090/S0002-9947-02-03091-X. Primary author text: https://arxiv.org/pdf/math/0112008, Theorem 1.1 and (1.2), p.1; nonnegative weights follow by the simple-function approximation described before (1.2). The precise representative is automatic for a continuous function, by the definition (2.5), p.5.

Only continuous real W1,2_loc functions on the plane and bounded Borel sets are used. The derivative is the actual distributional gradient. The proposition below contains no level topology or null image assertion.