OAI/Analysis/CircleDomains/Rigidity/MatchedRoundDisks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual round disk parameters for the countable exceptional matched component pairs. Both radius-square sums follow from their geometry.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.IndexedMatchedPair line 16
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.indexedMatchedPair_countable line 19
  3. structure OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks line 23
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.exists_matched_round_disks line 37