OAI/Analysis/CircleDomains/Sobolev/PeriodWeightedCoarea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual masked mean-period levels have finite weighted physical length almost everywhere, as required by the subsequent barrier step.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.ae_finite_weighted_levels line 17