Univalent Function Classes: classS and classSigma

We define the class S of normalized univalent functions on the unit disc and the class Σ of univalent functions on the exterior of the closed unit disk with the expansion g(z) = z + b₀ + b₁/z + ... at infinity. We then prove:

• For any function f in S, its square root transform g(z) = sqrt(f(z^2)) is also in S; square_root_transform_in_S. This involves proving the existence of an analytic square root of f(z)/z and verifying the properties of the transformed function.

• If f is in classS, then g(z) = 1/f(1/z) is in classSigma; inv_f_inv_in_Sigma.

Definitions

def LeanPool.LeanComplexAnalysis.classS : Set (ℂ → ℂ)

The class S consists of normalized analytic univalent functions on the unit disc.

Equations

• LeanPool.LeanComplexAnalysis.classS = {f : ℂ → ℂ | AnalyticOn ℂ f (Metric.ball 0 1) ∧ Set.InjOn f (Metric.ball 0 1) ∧ f 0 = 0 ∧ deriv f 0 = 1}

def LeanPool.LeanComplexAnalysis.classSigma : Set (ℂ → ℂ)

The class Sigma of analytic and injective functions on the complement of the closed unit disc with the expansion g(z) = z + b0 + b1/z + ...

Equations

• One or more equations did not get rendered due to their size.

Theorems

theorem LeanPool.LeanComplexAnalysis.analyticOn_dslope_of_analyticOn (f : ℂ → ℂ) : AnalyticOn ℂ f (Metric.ball 0 1) → AnalyticOn ℂ (dslope f 0) (Metric.ball 0 1)

If f is analytic on the unit disc, then dslope f 0 (= f(z)/z for z≠0, f'(z) for z=0) is also analytic on the unit disc.

theorem LeanPool.LeanComplexAnalysis.dslope_ne_zero_of_in_S (f : ℂ → ℂ) (hf : f ∈ classS) (z : ℂ) : z ∈ Metric.ball 0 1 → dslope f 0 z ≠ 0

For any function f in classS, the difference slope of f at 0 is non-zero everywhere on the unit disc.

noncomputable def LeanPool.LeanComplexAnalysis.primitiveOnBall (f : ℂ → ℂ) (z : ℂ) : ℂ

The primitive of a function f on the unit ball, defined as the integral along the segment from 0 to z.

Equations

• LeanPool.LeanComplexAnalysis.primitiveOnBall f z = z * ∫ (t : ℝ) in 0..1, f (↑t * z)

theorem LeanPool.LeanComplexAnalysis.hasDerivAt_integral_of_analytic_mul (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : HasDerivAt (fun (w : ℂ) => ∫ (t : ℝ) in 0..1, f (↑t * w)) (∫ (t : ℝ) in 0..1, deriv f (↑t * z) * ↑t) z

The derivative of the integral of f(t*w) with respect to w at z is the integral of f'(t*z)*t.

theorem LeanPool.LeanComplexAnalysis.hasDerivAt_primitiveOnBall (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball 0 1)) (z : ℂ) (hz : z ∈ Metric.ball 0 1) : HasDerivAt (primitiveOnBall f) (f z) z

The derivative of the primitive of f on the unit ball at z is f(z).

theorem LeanPool.LeanComplexAnalysis.analyticOn_primitiveOnBall (f : ℂ → ℂ) (hf : AnalyticOn ℂ f (Metric.ball 0 1)) : AnalyticOn ℂ (primitiveOnBall f) (Metric.ball 0 1)

The primitive of an analytic function on the unit ball is analytic on the unit ball.

theorem LeanPool.LeanComplexAnalysis.exists_log_of_analytic_nonzero_on_ball (f : ℂ → ℂ) (hf_anal : AnalyticOn ℂ f (Metric.ball 0 1)) (hf_ne_zero : ∀ z ∈ Metric.ball 0 1, f z ≠ 0) : ∃ (g : ℂ → ℂ), AnalyticOn ℂ g (Metric.ball 0 1) ∧ ∀ z ∈ Metric.ball 0 1, Complex.exp (g z) = f z

If f is a non-vanishing analytic function on the unit ball, then there exists an analytic function g on the unit ball such that exp(g(z)) = f(z).

theorem LeanPool.LeanComplexAnalysis.exists_sqrt_f_div_z (f : ℂ → ℂ) (hf : f ∈ classS) : ∃ (h : ℂ → ℂ), AnalyticOn ℂ h (Metric.ball 0 1) ∧ h 0 = 1 ∧ ∀ z ∈ Metric.ball 0 1, z ≠ 0 → h z ^ 2 = f z / z

For any function f in classS, there exists an analytic function h on the unit disc such that h(z)^2 = f(z)/z for non-zero z, and h(0) = 1.

theorem LeanPool.LeanComplexAnalysis.square_root_transform_in_S (f : ℂ → ℂ) (hf : f ∈ classS) : ∃ g ∈ classS, ∀ z ∈ Metric.ball 0 1, g z ^ 2 = f (z ^ 2)

The class S consists of normalized analytic univalent functions on the unit disc. The square root transform of f, defined by g(z) = sqrt(f(z^2)), is also in S.

theorem LeanPool.LeanComplexAnalysis.inv_f_sub_inv_id_analytic (f : ℂ → ℂ) (hf : f ∈ classS) : ∃ (h : ℂ → ℂ), AnalyticOn ℂ h (Metric.ball 0 1) ∧ ∀ z ∈ Metric.ball 0 1, z ≠ 0 → h z = 1 / f z - 1 / z

If f is in classS, then 1/f(z) - 1/z extends to an analytic function on the unit disk.

theorem LeanPool.LeanComplexAnalysis.inv_f_inv_analyticOn (f : ℂ → ℂ) (hf : f ∈ classS) : AnalyticOn ℂ (fun (z : ℂ) => 1 / f (1 / z)) {z : ℂ | 1 < ‖z‖}

The function 1/f(1/z) is analytic on the exterior of the unit disk.

theorem LeanPool.LeanComplexAnalysis.inv_f_inv_injOn (f : ℂ → ℂ) (hf : f ∈ classS) : Set.InjOn (fun (z : ℂ) => 1 / f (1 / z)) {z : ℂ | 1 < ‖z‖}

The function 1/f(1/z) is injective on the exterior of the unit disk.

theorem LeanPool.LeanComplexAnalysis.inv_f_inv_in_Sigma (f : ℂ → ℂ) (hf : f ∈ classS) : (fun (z : ℂ) => 1 / f (1 / z)) ∈ classSigma

If f is in classS, then g(z) = 1/f(1/z) is in classSigma.