OAI/Analysis/CircleDomains/Topology/CircleFiniteTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Analytic transfer of circle coordinates on the full completion

One sufficiently small good width gives simultaneous smooth fillings, core agreement, a common spherical-background metric, and total and localized energy bounds on the entire cofinite completed domain.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_circle_transfer_at_good_width line 20