OAI/Analysis/CircleDomains/Sobolev/CircleWeightedCoarea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two fixed cuts reduce the weighted-length estimate for a smooth circle coordinate to the published scalar coarea specialization.

  1. theorem OAI.CircleDomainRigidity.ae_finite_spherical_circle_weighted_levels line 17