WeightedPlanarCoareaProof.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The planar nonnegative weighted C1 coarea formula. The critical set is treated by diameter covers, and the regular set by actual inverse charts, curve arclength, Fubini and change of variables.

theorem OAI.CircleDomainRigidity.weightedPlanarScalarCoarea line 15
Source documentation
Federer's nonnegative weighted scalar planar coarea identity.
```
theorem weightedPlanarScalarCoarea : WeightedPlanarScalarCoarea := by
…
```
Mentions: OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea