OAI/Analysis/CircleDomains/Sobolev/SobolevLinePayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous compact Sobolev barriers pay for every transverse line on which they attain one. Uniform mollification supplies the line FTC; strong convergence of weak partials passes the energy bound to the limit.

  1. theorem OAI.CircleDomainRigidity.sobolev_coordinate_line_payment line 16