OAI/Analysis/CircleDomains/Modulus/AssignedStokesBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite model obeys the countable-band Stokes bound with its singular mark removed. Disjointness and containment of its round holes provide the radius budget; the source collar branches provide the boundary oscillations.

  1. theorem OAI.CircleDomainRigidity.assigned_model_stokes_band_bound line 17