OAI/Analysis/CircleDomains/Sobolev/SobolevBarrierCollapse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing global Sobolev energy excludes a positive measure family of coordinate crossings. The crossing locations may vary with every barrier.

  1. theorem OAI.CircleDomainRigidity.measure_zero_of_vanishing_sobolev_barriers line 12