OAI/Analysis/CircleDomains/Topology/CircleBoundaryPersistence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A retained real lift converts the actual target-circuit Stokes integral into the fixed-source boundary functional. Uniform convergence of the maps and convergence of the terminal disks then pass the proved finite Stokes bound to the limiting pair.

  1. theorem OAI.CircleDomainRigidity.circleFormIntegral_eq_roundBoundaryPairing line 19
  2. theorem OAI.CircleDomainRigidity.stokes_boundary_limit_bound line 28