Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-29
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.

Schwarz-Pick lemma on the unit disc

Statement

Let f:D→D be holomorphic. Then for every a,z∈D,

∣f(z)−f(a)1−f(a)‾ f(z)∣≤∣z−a1−a‾ z∣.

Equivalently,

∣φf(a)(f(z))∣≤∣φa(z)∣.

Moreover,

∣f′(a)∣≤1−∣f(a)∣21−∣a∣2(a∈D),

and if equality holds for some distinct a,z∈D or in the derivative inequality at some a∈D, then f is an automorphism of D.

Facts & Assumptions

Given: A holomorphic self-map f:D→D and points a,z∈D.

[F1]

Every Blaschke factor φc is an automorphism of D (Blaschke factors are automorphisms of the disc).

[F2]

A disc self-map fixing 0 satisfies Schwarz's lemma, with equality only for rotations (Schwarz lemma with the equality cases).

[F3]

Holomorphic compositions satisfy the chain rule (The chain rule for complex derivatives).

Proof

technique · direct
1.1F1givenconstruct

Put b=f(a) and F=φb∘f∘φa. By [F1], the two Blaschke factors are disc automorphisms, so F:D→D is holomorphic and satisfies F(0)=φb(f(a))=0.

2.1F1F2step 1.1algebra

Applying [F2] to F at the point φa(z)∈D gives ∣F(φa(z))∣≤∣φa(z)∣, that is, ∣φb(f(z))∣≤∣φa(z)∣. This is exactly the displayed pseudohyperbolic inequality.

2.2F2F3step 1.1algebra

Since φa′(0)=∣a∣2−1 and φb′(b)=−1/(1−∣b∣2), the chain rule [F3] gives ∣F′(0)∣=∣φb′(b)∣ ∣f′(a)∣ ∣φa′(0)∣=(1−∣a∣2)∣f′(a)∣/(1−∣b∣2). Applying the derivative part of [F2] to F yields the stated bound for ∣f′(a)∣.

3.1F1F2step 2.1step 2.2casesalgebra∎

If equality holds in the pseudohyperbolic inequality for some z≠a, then equality holds in Schwarz's lemma for F at the nonzero point φa(z); if equality holds in the derivative inequality, then ∣F′(0)∣=1. In either case [F2] makes F a rotation, so f=φb∘F∘φa is an automorphism by [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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