Robertson's conjecture on odd univalent functions

DefinitionOpen unit disc#✓fully proved

The open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\) in the complex plane.

def haymanUnitDisc : Set ℂ := {z | ‖z‖ < 1}

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Used by 4

Used byClose-to-convex functions · Normalized odd square roots · Normalized univalent functions (class \(S\)) · Starlike univalent functions

DefinitionNormalized univalent functions (class \(S\))#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) belongs to the class \(S\) when it is analytic at every point of the open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\), injective on \(\mathbb{D}\), and satisfies \(f(0) = 0\) and \(f'(0) = 1\).

def haymanIsSchlicht (f : ℂ → ℂ) : Prop :=
  AnalyticOnNhd ℂ f haymanUnitDisc ∧ Set.InjOn f haymanUnitDisc ∧
    f 0 = 0 ∧ HasDerivAt f 1 0

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 1 · Used by 3

Statement usesOpen unit disc

Used byRobertson's conjecture for real-coefficient and close-to-convex functions · Close-to-convex functions · Starlike univalent functions

DefinitionStarlike univalent functions#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) is starlike when it belongs to the class \(S\) (analytic at every point of the open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\), injective on \(\mathbb{D}\), \(f(0) = 0\) and \(f'(0) = 1\)) and \(\operatorname{Re}\bigl(z f'(z) / f(z)\bigr) > 0\) for every \(z \in \mathbb{D}\) with \(z \ne 0\).

noncomputable def haymanIsStarlike (f : ℂ → ℂ) : Prop :=
  haymanIsSchlicht f ∧
    ∀ z ∈ haymanUnitDisc, z ≠ 0 → 0 < (z * deriv f z / f z).re

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 2 · Used by 1

Statement usesNormalized univalent functions (class \(S\)) · Open unit disc

Used byClose-to-convex functions

DefinitionReal Taylor coefficients at the origin#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) has real Taylor coefficients at \(0\) when, for every natural number \(n\), the value \(f^{(n)}(0)\) of its \(n\)-th iterated derivative at \(0\) is real (equivalently, every Taylor coefficient \(f^{(n)}(0)/n!\) is real).

noncomputable def haymanHasRealCoeffs (f : ℂ → ℂ) : Prop :=
  ∀ n : ℕ, (Nat.iterate deriv n f 0).im = 0

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Used by 1

Used byRobertson's conjecture for real-coefficient and close-to-convex functions

DefinitionClose-to-convex functions#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) is close-to-convex when it belongs to the class \(S\) (analytic at every point of the open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\), injective on \(\mathbb{D}\), \(f(0) = 0\) and \(f'(0) = 1\)) and there are a starlike function \(g\) and a real number \(\alpha\) such that \(\operatorname{Re}\bigl(e^{i\alpha} z f'(z) / g(z)\bigr) > 0\) for every \(z \in \mathbb{D}\) with \(z \ne 0\). Here \(g\) is starlike when it belongs to \(S\) and \(\operatorname{Re}\bigl(z g'(z) / g(z)\bigr) > 0\) for every \(z \in \mathbb{D}\) with \(z \ne 0\).

noncomputable def haymanIsCloseToConvex (f : ℂ → ℂ) : Prop :=
  haymanIsSchlicht f ∧
    ∃ g : ℂ → ℂ, ∃ alpha : ℝ, haymanIsStarlike g ∧
      ∀ z ∈ haymanUnitDisc, z ≠ 0 →
        0 < (Complex.exp ((alpha : ℂ) * Complex.I) * z * deriv f z / g z).re

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 3 · Used by 1

Statement usesNormalized univalent functions (class \(S\)) · Starlike univalent functions · Open unit disc

Used byRobertson's conjecture for real-coefficient and close-to-convex functions

DefinitionNormalized odd square roots#✓fully proved

Given \(f : \mathbb{C} \to \mathbb{C}\), a function \(h : \mathbb{C} \to \mathbb{C}\) is a normalized odd square root \(h(z) = f(z^2)^{1/2}\) when, on the open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\), \(h\) is analytic at every point and satisfies \(h(z)^2 = f(z^2)\) and \(h(-z) = -h(z)\) for all \(z \in \mathbb{D}\), and moreover \(h(0) = 0\) and \(h'(0) = 1\).

def haymanIsOddSqrt (h f : ℂ → ℂ) : Prop :=
  AnalyticOnNhd ℂ h haymanUnitDisc ∧
    (∀ z ∈ haymanUnitDisc, h z ^ 2 = f (z ^ 2)) ∧
    (∀ z ∈ haymanUnitDisc, h (-z) = -h z) ∧ h 0 = 0 ∧ HasDerivAt h 1 0

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 1 · Used by 1

Statement usesOpen unit disc

Used byRobertson's conjecture for real-coefficient and close-to-convex functions

DefinitionTaylor coefficients at the origin#✓fully proved

For a function \(h : \mathbb{C} \to \mathbb{C}\) and a natural number \(n\), \(c_n(h) = h^{(n)}(0) / n!\), where \(h^{(n)}\) is the \(n\)-th iterated derivative of \(h\). For \(h\) analytic near \(0\) this is the \(n\)-th Taylor coefficient of \(h\) at \(0\); Robertson's problem uses it at odd \(n\).

noncomputable def haymanOddSqrtCoeff (h : ℂ → ℂ) (n : ℕ) : ℂ :=
  Nat.iterate deriv n h 0 / (Nat.factorial n : ℂ)

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Used by 1

Used byRobertson's bound

DefinitionRobertson's bound#✓fully proved

For a function \(h : \mathbb{C} \to \mathbb{C}\) with Taylor coefficients \(c_k = h^{(k)}(0)/k!\) at \(0\) and a natural number \(n\), the Robertson bound for \(h\) at \(n\) is the inequality \(|c_1|^2 + |c_3|^2 + \dots + |c_{2n-1}|^2 \le n\) (for \(n = 0\) the sum is empty).

noncomputable def haymanRobertsonBound (h : ℂ → ℂ) (n : ℕ) : Prop :=
  ∑ k ∈ Finset.range n, ‖haymanOddSqrtCoeff h (2 * k + 1)‖ ^ 2 ≤ (n : ℝ)

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 1 · Used by 1

Statement usesTaylor coefficients at the origin

Used byRobertson's conjecture for real-coefficient and close-to-convex functions

DefinitionRobertson's conjecture for real-coefficient and close-to-convex functions#✓fully proved

Let \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\). The statement that for all functions \(f, h : \mathbb{C} \to \mathbb{C}\) such that \(f\) belongs to the class \(S\) (analytic at every point of \(\mathbb{D}\), injective on \(\mathbb{D}\), \(f(0) = 0\) and \(f'(0) = 1\)), \(h\) is a normalized odd square root of \(f(z^2)\) (analytic at every point of \(\mathbb{D}\), with \(h(z)^2 = f(z^2)\) and \(h(-z) = -h(z)\) for all \(z \in \mathbb{D}\), \(h(0) = 0\) and \(h'(0) = 1\)), and \(f\) has real Taylor coefficients at \(0\) or is close-to-convex, the Taylor coefficients \(c_k = h^{(k)}(0)/k!\) of \(h\) at \(0\) satisfy \(|c_1|^2 + |c_3|^2 + \dots + |c_{2n-1}|^2 \le n\) for every integer \(n \ge 1\).

Resolved true: de Branges (1985) proved the bound for every function in \(S\) via the Milin conjecture.

noncomputable def conjecture : Prop :=
  (∀ f h : ℂ → ℂ, haymanIsSchlicht f → haymanHasRealCoeffs f →
    haymanIsOddSqrt h f → ∀ n : ℕ, 1 ≤ n → haymanRobertsonBound h n) ∧
  (∀ f h : ℂ → ℂ, haymanIsSchlicht f → haymanIsCloseToConvex f →
    haymanIsOddSqrt h f → ∀ n : ℕ, 1 ≤ n → haymanRobertsonBound h n)

Sources

• AMR-022-6039, Hayman Problem 6.39, arXiv:1809.07200.

Uses 5 · Used by 1

Statement usesReal Taylor coefficients at the origin · Close-to-convex functions · Normalized odd square roots · Normalized univalent functions (class \(S\)) · Robertson's bound

Used byRobertson's conjecture holds for real-coefficient and close-to-convex functions

TheoremRobertson's conjecture holds for real-coefficient and close-to-convex functions#●ready to prove

Let \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\). For all functions \(f, h : \mathbb{C} \to \mathbb{C}\) such that \(f\) belongs to the class \(S\) (analytic at every point of \(\mathbb{D}\), injective on \(\mathbb{D}\), \(f(0) = 0\) and \(f'(0) = 1\)), \(h\) is a normalized odd square root of \(f(z^2)\) (analytic at every point of \(\mathbb{D}\), with \(h(z)^2 = f(z^2)\) and \(h(-z) = -h(z)\) for all \(z \in \mathbb{D}\), \(h(0) = 0\) and \(h'(0) = 1\)), and \(f\) has real Taylor coefficients at \(0\) or is close-to-convex, the Taylor coefficients \(c_k = h^{(k)}(0)/k!\) of \(h\) at \(0\) satisfy \(|c_1|^2 + |c_3|^2 + \dots + |c_{2n-1}|^2 \le n\) for every integer \(n \ge 1\).

De Branges' 1985 proof of the Milin conjecture implies the Robertson bound for every normalized univalent function, hence for the real-coefficient and close-to-convex subclasses formalized here.

public theorem_wanted conjecture_holds : conjecture

Sources

• de Branges, L., A proof of the Bieberbach conjecture, Acta Math. 154 (1985), 137-152, https://doi.org/10.1007/BF02392821.

Uses 1

Statement usesRobertson's conjecture for real-coefficient and close-to-convex functions

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.