FiniteUniformization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The published finite circle-uniformization input

Conway, Functions of One Complex Variable II, GTM 159 (1995), Theorem 15.7.9, p. 106, gives circle uniformization of nondegenerate finitely connected regions. FiniteCircleUniformization records only its existence conclusion on the sphere, omitting normalization and uniqueness. It is an explicit proposition parameter, not an axiom.

The complement components of a finite family of disjoint closed connected sets are identified below. This checks the finiteness and nondegeneracy hypotheses for completed surfaces, also after an arbitrary sphere homeomorphism such as compact metric uniformization.

def OAI.CircleDomainRigidity.FiniteNondegenerateComplement line 28
def OAI.CircleDomainRigidity.FiniteCircleUniformization line 32
theorem OAI.CircleDomainRigidity.connectedComponentIn_finite_disjoint_closed line 38
theorem OAI.CircleDomainRigidity.finite_nondegenerate_complement_of_disjoint_closed line 69
theorem OAI.CircleDomainRigidity.circle_model_of_finite_disjoint_complement line 88

theorem OAI.CircleDomainRigidity.circle_model_after_homeomorphism line 110

Source documentation

After compact metric uniformization, the finite circle theorem gives an actual bijection to a circle domain. It is conformal in every region where the metric uniformization retained the original complex structure.

theorem circle_model_after_homeomorphism
    (hfinite : FiniteCircleUniformization)
    {I : Type*} [Finite I] {U W : Set Sphere} (hU : IsOpen U) (hconnU : IsConnected U)
    (C : I → Set Sphere) (hC : ∀ i, IsClosed (C i))
    (hconn : ∀ i, IsPreconnected (C i)) (hdisj : Pairwise (Disjoint on C))
    (hneq : ∀ i, (C i).Nontrivial) (hcomp : Uᶜ = ⋃ i, C i)
    (e : Sphere ≃ₜ Sphere) (hW : W ⊆ U) (he : IsConformalOn e W) :
    ∃ (V : Set Sphere) (f : Sphere → Sphere),
      IsCircleDomain V ∧ BijOn f U V ∧ IsConformalOn f W ∧
        IsConformalEquivalence (f ∘ e.symm) (e '' U) V := by
…

Mentions: OAI.CircleDomainRigidity.FiniteCircleUniformization, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsConformalOn, OAI.CircleDomainRigidity.IsCircleDomain, OAI.CircleDomainRigidity.IsConformalEquivalence