OAI/Analysis/CircleDomains/Topology/SourceCollarStokes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The numerical source-energy bound on an actual image of a retained source collar. All target holes and the regular image circuit are derived.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.source_collar_stokes_bound line 15