OAI/Analysis/CircleDomains/Rigidity/ActualEnclosedCircleSlice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact finite-circle slice inequality for the selected matched field and the actual zero-extended source differential.

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