LeanPool.RiemannMappingTheorem.Main

theorem IsCompact_𝓙 {U : Set ℂ} [good_domain U] : IsCompact (𝓙 U)

noncomputable def obs {U : Set ℂ} (z₀ : ℂ) (f : 𝓒 U) : ℝ

The objective functional obs z₀ f = ‖f'(z₀)‖ whose maximisation over 𝓘 U produces the Riemann-mapping conformal isomorphism.

Equations

• obs z₀ f = ‖deriv f z₀‖

theorem ContinuousOn_obs {U : Set ℂ} {z₀ : ℂ} (hU : IsOpen U) (hz₀ : z₀ ∈ U) : ContinuousOn (obs z₀) (𝓗 U)

theorem main {U : Set ℂ} [good_domain U] : ∃ f ∈ 𝓘 U, f '' U = Metric.ball 0 1

theorem RMT {U : Set ℂ} (h1 : IsOpen U) (h2 : IsConnected U) (h3 : U ≠ Set.univ) (h4 : hasPrimitives U) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.InjOn f U ∧ f '' U = Metric.ball 0 1