OAI/Analysis/CircleDomains/Sobolev/PhysicalCircleSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive smoothing of the actual circle-valued mean of the physical arc law. Every local Sobolev witness is derived from occupation and coarea; the smoothing discrepancy obeys the prescribed pointwise tolerance.

  1. theorem OAI.CircleDomainRigidity.physical_mean_circle_smoothing line 23