OAI/Analysis/CircleDomains/Rigidity/MatchedSliceEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The numerical slice estimate for the actual matched correspondence. Only disks meeting the segment are charged.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.scalar_slice_estimate line 19