Conformal.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Sphere conformality and circle-domain statements

The concrete Riemann-sphere charts define conformal equivalences, round disks, and conformal removability. The two circle-domain statements express unrestricted uniformization and rigidity under removability.

theorem OAI.CircleDomainRigidity.sphereInv_involutive line 21
Source documentation
Sphere inversion exchanges zero and infinity and is its own inverse.
```
theorem sphereInv_involutive : Function.Involutive sphereInv := by
…
```
Mentions: OAI.CircleDomainRigidity.sphereInv
theorem OAI.CircleDomainRigidity.sphereInv_sphereInv line 31
theorem OAI.CircleDomainRigidity.chart_chartSymm line 35
Source documentation
The concrete chart and inverse chart are inverse at all finite chart values.
```
theorem chart_chartSymm (p : Sphere) (z : ℂ) :
    chart p (chartSymm p z) = z := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.chart, OAI.CircleDomainRigidity.chartSymm
theorem OAI.CircleDomainRigidity.isConformalAt_id line 42
Source documentation
The identity is conformal in both finite and infinite charts.
```
theorem isConformalAt_id (p : Sphere) : IsConformalAt id p := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsConformalAt
theorem OAI.CircleDomainRigidity.isConformalEquivalence_id line 49
Source documentation
Reflexivity of the concrete conformal-equivalence predicate.
```
theorem isConformalEquivalence_id (U : Set Sphere) :
    IsConformalEquivalence id U U := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsConformalEquivalence
def OAI.CircleDomainRigidity.KoebeCircleDomainConjecture line 59
Source documentation
Paper 047-02, Introduction, thm:main: unrestricted Koebe uniformization.
```
def KoebeCircleDomainConjecture : Prop :=
…
```
def OAI.CircleDomainRigidity.CircleDomainRemovabilityRigidity line 65
Source documentation
Paper 047-01, Introduction, thm:main: removability implies rigidity.
```
def CircleDomainRemovabilityRigidity : Prop :=
…
```
theorem OAI.CircleDomainRigidity.circleDomainModel_univ line 72
Source documentation
The whole-sphere case of Koebe uniformization.
```
theorem circleDomainModel_univ :
    ∃ (V : Set Sphere) (f : Sphere → Sphere),
      IsCircleDomain V ∧ IsConformalEquivalence f univ V :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsCircleDomain, OAI.CircleDomainRigidity.IsConformalEquivalence
theorem OAI.CircleDomainRigidity.circleDomainModel_of_circleDomain line 78
Source documentation
An already circular domain is its own conformal model.
```
theorem circleDomainModel_of_circleDomain {U : Set Sphere} (hU : IsCircleDomain U) :
    ∃ (V : Set Sphere) (f : Sphere → Sphere),
      IsCircleDomain V ∧ IsConformalEquivalence f U V :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsCircleDomain, OAI.CircleDomainRigidity.IsConformalEquivalence