OAI/Analysis/CircleDomains/Reflection/RoundExteriorBoundaryChart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

An explicit holomorphic chart from the upper half-disk to the exterior side of a round boundary.

  1. def OAI.CircleDomainRigidity.unitExteriorBoundaryChart line 12
  2. def OAI.CircleDomainRigidity.roundExteriorBoundaryChart line 14
  3. lemma OAI.CircleDomainRigidity.unitExteriorBoundaryChart_zero line 17
  4. lemma OAI.CircleDomainRigidity.cayley_ne_zero_of_norm_lt_one line 20
  5. lemma OAI.CircleDomainRigidity.cayley_den_ne_zero_of_norm_lt_one line 31
  6. lemma OAI.CircleDomainRigidity.differentiableAt_unitExteriorBoundaryChart line 37
  7. lemma OAI.CircleDomainRigidity.unitExteriorBoundaryChart_norm_gt_one line 43
  8. lemma OAI.CircleDomainRigidity.unitExteriorBoundaryChart_norm_eq_one line 49
  9. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_norm line 53
  10. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_differentiable line 58
  11. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_exterior line 62
  12. lemma OAI.CircleDomainRigidity.roundExteriorBoundaryChart_boundary line 68