LeanPool.RiemannMappingTheorem.Etape2

theorem one_sub_mul_conj_ne_zero {z u : ℂ} (hu : u ∈ 𝔻) (hz : z ∈ 𝔻) : 1 - z * (starRingEnd ℂ) u ≠ 0

theorem one_sub_mul_conj_add_mul_conj_ne_zero {z u : ℂ} (hu : u ∈ 𝔻) : 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u ≠ 0

theorem normSq_sub_normSq {z u : ℂ} : Complex.normSq (z - u) - Complex.normSq (1 - z * (starRingEnd ℂ) u) = (Complex.normSq z - 1) * (1 - Complex.normSq u)

noncomputable def preΦ (u z : ℂ) : ℂ

The Möbius transformation preΦ u z = (z - u) / (1 - z·ū) underlying the disk automorphism φ. Maps 𝔻 to itself when u ∈ 𝔻.

Equations

• preΦ u z = (z - u) / (1 - z * (starRingEnd ℂ) u)

theorem pre_φ_inv {u : ℂ} (hu : u ∈ 𝔻) : Set.LeftInvOn (preΦ (-u)) (preΦ u) 𝔻

noncomputable def φ {u : ℂ} (hu : u ∈ 𝔻) : embedding 𝔻 𝔻

The disk automorphism φ u : 𝔻 → 𝔻 packaged as an embedding. Equals preΦ u and sends u ↦ 0.

Equations

• φ hu = { toFun := fun (z : ℂ) => (z - u) / (1 - z * (starRingEnd ℂ) u), is_diff := ⋯, is_inj := ⋯, maps_to := ⋯ }

theorem φ_deriv {z u : ℂ} (hu : u ∈ 𝔻) (hz : z ∈ 𝔻) : deriv (φ hu).toFun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2

theorem φ_inv {z u : ℂ} (hu : u ∈ 𝔻) (hz : z ∈ 𝔻) : (φ ⋯).toFun ((φ hu).toFun z) = z

theorem non_injective_schwarz {f : ℂ → ℂ} (f_diff : DifferentiableOn ℂ f 𝔻) (f_img : Set.MapsTo f 𝔻 𝔻) (f_noninj : ¬Set.InjOn f 𝔻) : ‖deriv f 0‖ < 1

theorem step_2 {z₀ : ℂ} (U : Set ℂ) [good_domain U] (hz₀ : z₀ ∈ U) (f : embedding U 𝔻) (hf : f.toFun '' U ⊂ 𝔻) : ∃ (h : embedding U 𝔻), ‖deriv f.toFun z₀‖ < ‖deriv h.toFun z₀‖