OAI/Analysis/CircleDomains/Rigidity/ActualAxialCircleFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-hole axial flux bound from the proved common-point trace and the source differential.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.actual_axial_circle_flux line 20