OAI/Analysis/CircleDomains/Rigidity/ConditionalFiniteFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-hole flux from axial slice estimates, multiplicity bounds, circle integration, and shrinking-hole limits. The outer principal flux is an explicit hypothesis.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.finite_flux_of_published_inputs line 22