OAI/Analysis/CircleDomains/Uniformization/MixedStokesLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed-source exclusion for an actual mixed model sequence. Smoothness, mask containment, a common lifted coordinate and the uniform error are derived from retention and local uniform convergence.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.excludes_source_stokes_limit line 17