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.

The sine map biholomorphically sends an upper half-strip onto the upper half-plane

Statement

Let

$S : = {z \in C : - π / 2 < Re z < π / 2, Im z > 0} .$

Then the sine map

$\sin : S \to H$

is a biholomorphism onto the upper half-plane $H = {w \in C : Im w > 0}$ .

Facts & Assumptions

Given: The upper half-strip $S$ above.

[F1]

The exponential is a biholomorphism from the principal strip $P = {u \in C : - π < Im u < π}$ onto the slit plane $C ∖ {x \in R : x \leq 0}$ , with inverse the principal logarithm (The exponential is the inverse biholomorphism from the principal strip to the slit plane).

[F2]

The Joukowski map $J (η) = \frac{1}{2} (η + η^{- 1})$ is a biholomorphism from ${∣ η ∣ > 1}$ onto $C ∖ [- 1, 1]$ (The Joukowski map is a biholomorphism from the exterior disc onto $C ∖ [- 1, 1]$ ).

[F3]

Complex sine is defined by $\sin z = \frac{\exp (i z) - \exp (- i z)}{2 i}$ (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).

Proof

technique · direct

1.1F1givenconstructalgebra

Fix $z \in S$ and put $q : = \exp (i z)$ . Since $i z$ has real part $- Im z < 0$ and imaginary part $Re z \in (- π / 2, π / 2) \subset (- π, π)$ , [F1] gives $q$ in the slit plane with $∣ q ∣ < 1$ and $Re q > 0$ . Define $η : = - i / q$ ; then $∣ η ∣ > 1$ and $Im η = - Re q / ∣ q ∣^{2} < 0$ .

2.1F2F3step 1.1algebra

By [F3], $\sin z = (q - q^{- 1}) / (2 i) = - (η + η^{- 1}) / 2 = - J (η)$ . For $η = u + i v$ with $∣ η ∣ > 1$ , one has $Im J (η) = \frac{1}{2} (v - \frac{v}{u^{2} + v^{2}}) = \frac{v}{2} (1 - \frac{1}{∣ η ∣^{2}})$ , so step 1.1 gives $Im J (η) < 0$ and therefore $Im \sin z > 0$ . Hence $\sin [S] \subseteq H$ .

3.1F1F2step 2.1givenconstructalgebra

Conversely, let $w \in H$ . Since $- w \in C ∖ [- 1, 1]$ , [F2] supplies a unique $η \in {∣ η ∣ > 1}$ with $J (η) = - w$ . The imaginary-part formula from step 2.1 shows $Im η$ has the same sign as $Im J (η) = - Im w < 0$ , so $Im η < 0$ . Put $q : = - i / η$ ; then $∣ q ∣ < 1$ and $Re q = - Im η / ∣ η ∣^{2} > 0$ , so $q$ lies in the right half-disc. By [F1], $u : = Log q$ belongs to the principal strip, with $Re u = \log ∣ q ∣ < 0$ and $Im u \in (- π / 2, π / 2)$ . Therefore $z : = - i u$ lies in $S$ .

4.1F1F2F3step 3.1algebra

For the point $z$ of step 3.1, [F1] gives $\exp (i z) = q$ , so the identity of step 2.1 yields $\sin z = - J (- i / q) = - J (η) = w$ . Thus $\sin : S \to H$ is surjective.

5.1F1F2F3step 3.1step 4.1∎

If $z_{1}, z_{2} \in S$ and $\sin z_{1} = \sin z_{2}$ , step 2.1 gives $J (η_{1}) = J (η_{2})$ for $η_{j} : = - i \exp (- i z_{j})$ . By [F2], $η_{1} = η_{2}$ , so $\exp (i z_{1}) = \exp (i z_{2})$ . Because each $i z_{j}$ lies in the principal strip, [F1] makes the exponential injective there, and hence $z_{1} = z_{2}$ . Therefore $\sin$ is bijective. Its inverse is the holomorphic composition $w \mapsto - i Log (- i / K (- w))$ , where $K$ is the holomorphic inverse supplied by [F2]. Thus $\sin : S \to H$ is a biholomorphism.

Depends on

Used by

Boundary tracking for the sine biholomorphism of the upper half-strip Example

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

Lars V. Ahlfors, Complex Analysis, 3rd ed., Ch. 3 §4.2 (standard reference, not scraped)
Elias M. Stein and Rami Shakarchi, Complex Analysis, Ch. 8 §1.2 (standard reference, not scraped)