OAI/Analysis/CircleDomains/Rigidity/ActualFiniteCircleFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Adding the two actual axial inequalities gives the full outward circle flux, with exactly sixteen times the remaining mixed-radius sum.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.actual_finite_circle_flux line 15