OAI/Analysis/CircleDomains/Modulus/NormalizedMarkedModels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalized limits with actual marked complementary disks

The marked components may only appear eventually in the finite models. A common subsequence yields their round Hausdorff limits and a two-sided conformal sphere limit. Hurwitz puts every limiting disk in the complement of that image. Assignment to a particular end is a separate geometric step.

  1. theorem OAI.CircleDomainRigidity.not_constant_on_open_of_conformal_extension line 22
  2. theorem OAI.CircleDomainRigidity.exists_normalized_marked_sphere_limit_with_parameters line 36
  3. theorem OAI.CircleDomainRigidity.exists_normalized_marked_sphere_limit line 115