OAI/Analysis/CircleDomains/Modulus/NonsingularStokesBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite Stokes bound consumes only nonsingular terminal excess. No oscillation or real lift is required at the distinguished terminal.

  1. theorem OAI.CircleDomainRigidity.assigned_model_stokes_nonsingular_bound line 14