OAI/Analysis/CircleDomains/Sobolev/AnnulusStokes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The zero-offset Stokes estimate on a finite circularly punctured Jordan region. Actual small-collar real lifts supply the nonsingular boundary data; the distinguished period is constructed on the annulus.

  1. theorem OAI.CircleDomainRigidity.finite_annulus_stokes_bound line 17