OAI/Analysis/CircleDomains/Rigidity/MatchedScalarIntervals.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual intervals for the matched disks. Their lengths are square summable and their centers represent values of the closed correspondence. Unused natural codes are harmless shrinking intervals at one fixed fiber.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.source_center_mem line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.target_center_mem line 23
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.centers_related line 28
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.scalar_fiber_bound line 34
  5. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceCenter line 48
  6. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceRadius line 51
  7. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceTargetRadius line 54
  8. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceScalarCenter line 57
  9. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceWidth line 62
  10. def OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceInterval line 65
  11. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceWidth_pos line 71
  12. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceWidth_summable_sq line 76
  13. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceWidth_tendsto line 84
  14. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceInterval_length line 89
  15. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceInterval_summable_sq line 96
  16. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.traceInterval_represents line 102