OAI/Analysis/CircleDomains/Rigidity/PrincipalCircleFluxLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual analytic principal germ gives the limiting vertical boundary flux. No boundary estimate is assumed: continuity of the analytic remainder supplies a uniform bound on inverse circles.

  1. theorem OAI.CircleDomainRigidity.inverse_circle_remainder_bound line 15
  2. theorem OAI.CircleDomainRigidity.principal_circle_flux_estimate line 39
  3. theorem OAI.CircleDomainRigidity.principal_circle_flux_limit line 76