LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Maximizing-point rescaling produces a normalized map with uniformly bounded derivative

Statement

Let $f$ be holomorphic on $D$ with $f^{'} (0) \neq 0$ , let $R : = 1 / 2$ , and let $Φ (z) : = (R - ∣ z ∣) ∣ f^{'} (z) ∣$ on $∣ z ∣ \leq R$ . If $z_{0}$ maximizes $Φ$ on the closed radius- $R$ disc and

$r : = \frac{R - ∣ z_{0} ∣}{2}, g (w) : = \frac{f (z_{0} + r w) - f (z_{0})}{r f^{'} (z_{0})},$

then $g$ is holomorphic on $D$ , satisfies $g (0) = 0$ and $g^{'} (0) = 1$ , obeys $∣ g^{'} (w) ∣ \leq 2$ for $∣ w ∣ < 1$ , and

$r ∣ f^{'} (z_{0}) ∣ \geq \frac{R ∣ f^{'} (0) ∣}{2} .$

Facts & Assumptions

Given: A holomorphic map $f : D \to C$ with $f^{'} (0) \neq 0$ , the radius $R = 1 / 2$ , and a maximizer $z_{0}$ of $Φ (z) = (R - ∣ z ∣) ∣ f^{'} (z) ∣$ on $∣ z ∣ \leq R$ .

[L1]

A continuous real-valued function on a nonempty compact metric space has a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

Proof

technique · direct

1.1

The closed disc $∣ z ∣ \leq R$ is compact, and $z \mapsto ∣ f^{'} (z) ∣$ is continuous, so [L1] justifies the maximizing point $z_{0}$ . Since $∣ z_{0} ∣ + r = (R + ∣ z_{0} ∣) / 2 < R$ , the affine disc $z_{0} + r D$ lies in $D$ , so $g$ is holomorphic on $D$ and direct differentiation gives $g (0) = 0$ , $g^{'} (0) = 1$ .

L1givenalgebra

2.1

If $∣ w ∣ < 1$ , then $∣ z_{0} + r w ∣ \leq ∣ z_{0} ∣ + r < R$ . Maximality of $z_{0}$ yields $(R - ∣ z_{0} + r w ∣) ∣ f^{'} (z_{0} + r w) ∣ \leq (R - ∣ z_{0} ∣) ∣ f^{'} (z_{0}) ∣ = 2 r ∣ f^{'} (z_{0}) ∣$ . Because $R - ∣ z_{0} + r w ∣ \geq R - ∣ z_{0} ∣ - r = r$ , dividing gives $∣ g^{'} (w) ∣ = ∣ f^{'} (z_{0} + r w) ∣ / ∣ f^{'} (z_{0}) ∣ \leq 2$ .

step 1.1algebra

3.1

Since $0$ lies in the maximizing disc, maximality also gives $R ∣ f^{'} (0) ∣ \leq (R - ∣ z_{0} ∣) ∣ f^{'} (z_{0}) ∣ = 2 r ∣ f^{'} (z_{0}) ∣$ , which is the claimed lower bound.

givenstep 1.1algebra∎

Depends on

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value

Used by

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Matthias Weber, Complex Analysis, §7.4 (standard reference, not scraped)