Holomorphic maps from the disc into a strip

AbbreviationThe open unit disc \(D\)#✓fully proved

The set \(D=\{z\in\mathbb{C}:|z|<1\}\) is the open disc of radius \(1\) about \(0\).

abbrev D : Set ℂ := Metric.ball (0 : ℂ) 1

Used by 1

Used byGrowth bound for holomorphic maps from the unit disc into a vertical strip

TheoremGrowth bound for holomorphic maps from the unit disc into a vertical strip#●ready to prove

Let \(D=\{z:|z|<1\}\subset\mathbb{C}\) be the unit disk and \(g:D\to\mathbb{C}\) be a holomorphic function such that \(g(0)=0\) and \(|\operatorname{Re} g(z)|<1\) for any \(z\in D\). Then for any \(z\in D\), [ |g(z)|\le \frac{2}{\pi}\log\frac{1+|z|}{1-|z|}. ]

public theorem_wanted norm_le_two_div_pi_mul_log_of_abs_re_lt_one
  (g : ℂ → ℂ)
  (hg_holo : DifferentiableOn ℂ g D)
  (hg0 : g 0 = 0)
  (hRe : ∀ z : ℂ, z ∈ D → |(Complex.re (g z))| < 1) :
  ∀ z : ℂ,
    z ∈ D →
      ‖g z‖ ≤ (2 / Real.pi) * Real.log ((1 + ‖z‖) / (1 - ‖z‖))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functions of a complex variable; Geometric function theory), problem ma_proofbench_l2_86.

Uses 1

Statement usesThe open unit disc \(D\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.