LeanPool.RiemannMappingTheorem.HasSqrt

def hasSqrt (U : Set ℂ) : Prop

hasSqrt U : every nowhere-zero holomorphic function on U has a holomorphic square root there.

Equations

• hasSqrt U = ∀ (f : ℂ → ℂ), (∀ z ∈ U, f z ≠ 0) → DifferentiableOn ℂ f U → ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g U ∧ Set.EqOn f (g ^ 2) U

def hasPrimitives (U : Set ℂ) : Prop

hasPrimitives U : every holomorphic function on U has a holomorphic primitive there.

Equations

• hasPrimitives U = ∀ (f : ℂ → ℂ), DifferentiableOn ℂ f U → ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g U ∧ Set.EqOn (deriv g) f U

def hasLogs (U : Set ℂ) : Prop

hasLogs U : every nowhere-zero holomorphic function on U has a holomorphic logarithm there.

Equations

• hasLogs U = ∀ (f : ℂ → ℂ), DifferentiableOn ℂ f U → (∀ z ∈ U, f z ≠ 0) → ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g U ∧ Set.EqOn f (Complex.exp ∘ g) U

theorem EqOn_zero_of_deriv_eq_zero {z₀ : ℂ} {U : Set ℂ} (hU : IsOpen U) (hU' : IsPreconnected U) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hf' : Set.EqOn (deriv f) 0 U) (hz₀ : z₀ ∈ U) (hfz₀ : f z₀ = 0) : Set.EqOn f 0 U

theorem EqOn_of_deriv_eq_zero {z₀ : ℂ} {U : Set ℂ} (hU : IsOpen U) (hU' : IsPreconnected U) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hf' : Set.EqOn (deriv f) 0 U) (hz₀ : z₀ ∈ U) : Set.EqOn f (fun (x : ℂ) => f z₀) U

theorem EqOn_of_EqOn_deriv {z₀ : ℂ} {U : Set ℂ} {f g : ℂ → ℂ} (hU : IsOpen U) (hU' : IsPreconnected U) (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) (hfg : Set.EqOn (deriv f) (deriv g) U) (hz₀ : z₀ ∈ U) (hfgz₀ : f z₀ = g z₀) : Set.EqOn f g U

theorem hasLogs.hasSqrt {U : Set ℂ} (h : hasLogs U) : _root_.hasSqrt U

theorem hasPrimitives.hasLogs {U : Set ℂ} (hp : hasPrimitives U) (hU : IsOpen U) (hU' : IsPreconnected U) : _root_.hasLogs U