OAI/Analysis/CircleDomains/Sobolev/SphericalWeightedCoarea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite spherical weighted length of almost every circle-valued level, from exactly the published scalar planar coarea input.

  1. theorem OAI.CircleDomainRigidity.ae_finite_spherical_weighted_levels line 19