OAI/Analysis/CircleDomains/Sobolev/PotentialPhysicalSmoothing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual physical-domain smoothing with global energy and all quotient bands.

  1. theorem OAI.CircleDomainRigidity.potential_physical_smoothing line 18