LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

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 Ahlfors-Beurling extension formula for quasisymmetric maps of the line

Statement

Assume the Axiom of Choice. Let $h : R \to R$ be an increasing $L$ -quasisymmetric homeomorphism, $L \geq 1$ (Quasisymmetric homeomorphisms of the line and circle), and let $H = {z \in C : Im z > 0}$ (The unit disc, the upper half-plane, and Blaschke factors, A complex domain is a nonempty connected open subset of $C$ ). For $x + i y \in H$ , define

$H (x + i y) = \frac{1}{2 y} \int_{x - y}^{x + y} h (t) d t + \frac{i}{y} (\int_{x}^{x + y} h (t) d t - \int_{x - y}^{x} h (t) d t) .$

Then:

(a) $H$ is continuously differentiable on $H$ , maps $H$ into $H$ , and extends continuously to $\overline{H}$ with boundary values $H (x) = h (x)$ .

(b) The real Jacobian determinant $J_{H}$ is positive everywhere on $H$ , so $H$ is a local diffeomorphism.

(c) With $C (L) : = 14 L^{3} (1 + L)$ and $k (L) : = \sqrt{(C (L) - 2) / (C (L) + 2)} < 1$ , the Wirtinger derivatives satisfy $∣ H_{\overset{ˉ}{z}} ∣ \leq k (L) ∣ H_{z} ∣$ on $H$ .

(d) $H$ is a homeomorphism $H \to H$ . Pasting $H$ on $\overline{H}$ to $H^{*} (z) : = \overline{H (\overset{ˉ}{z})}$ on the lower half-plane gives a $K (L)$ -quasiconformal homeomorphism of $\hat{C}$ preserving $R \cup {\infty}$ , where $K (L) = (1 + k (L)) / (1 - k (L))$ .

(e) If $\tilde{h} (x) = λ h (x / λ) + b$ for $λ > 0$ and $b \in R$ , then its extension is $\tilde{H} (z) = λ H (z / λ) + b$ .

Facts & Assumptions

Given: AC, an increasing $L$ -quasisymmetric homeomorphism $h : R \to R$ , $L \geq 1$ , and the displayed formula.

[F1]

The line definition of $L$ -quasisymmetry gives adjacent equal intervals image-length ratios between $L^{- 1}$ and $L$ (Quasisymmetric homeomorphisms of the line and circle).

[F2]

The upper half-plane is a connected open subset of $C$ , hence a complex domain (The unit disc, the upper half-plane, and Blaschke factors, A complex domain is a nonempty connected open subset of $C$ ).

[F3]

If all real partial derivatives of a map exist near a point and are continuous there, the map is totally differentiable there with those partials as its derivative (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[F4]

A $C^{1}$ map with invertible derivative at a point is a local $C^{1}$ diffeomorphism there (The Euclidean inverse function theorem).

[F5]

For a real-differentiable complex map $f = u + i v$ , $f_{z} = \frac{1}{2} (u_{x} + v_{y}) + \frac{i}{2} (v_{x} - u_{y})$ , $f_{\overset{ˉ}{z}} = \frac{1}{2} (u_{x} - v_{y}) + \frac{i}{2} (v_{x} + u_{y})$ , and $J_{f} = ∣ f_{z} ∣^{2} - ∣ f_{\overset{ˉ}{z}} ∣^{2}$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[F6]

AC implies Countable Choice (AC implies DC implies countable choice). Under these assumptions the ACL/Sobolev analytic definition of quasiconformality and the line-removability gluing theorem apply (The ACL and Sobolev analytic definition of quasiconformality, Compact subsets of lines and round circles are removable for quasiconformal maps).

[F7]

A proper $C^{1}$ local diffeomorphism between nonempty Euclidean open sets, with connected target, is surjective and has evenly covered neighbourhoods with finitely many diffeomorphic sheets (Proper maps between Euclidean open sets, A proper Euclidean local diffeomorphism has finite diffeomorphic sheets near every target point, Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

[F8]

A connected covering of a locally path-connected simply connected space is one-sheeted (A connected covering of a locally path-connected simply connected space is one-sheeted and trivial). Every convex domain $D$ is simply connected: fixing $z_{0} \in D$ , the homotopy $H (s, z) = (1 - s) z + s z_{0}$ stays in $D$ by convexity and contracts every loop to $z_{0}$ .

[F9]

Continuous real-valued functions on nonempty compact metric spaces attain their extrema; closed boxes in $R^{2}$ are compact and closed subsets of compact metric spaces are compact (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A closed subset of a compact metric space is compact).

[F10]

A continuous function on a compact metric space is uniformly continuous, compact subsets of metric spaces are closed and bounded, and bounded Lebesgue measurable subsets of $R^{2}$ , in particular compact rectangles, have finite Lebesgue measure (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, A compact subset of a metric space is closed and bounded, Lebesgue measure is sigma-finite, and every metrically bounded subset of $R^{n}$ has finite outer measure).

[F11]

Classical $C^{1}$ derivatives are weak derivatives under Countable Choice; a continuous injection from an open subset of $R^{2}$ into $R^{2}$ is open; and $\hat{C}$ has the one-point compactification topology (Classical derivatives agree with weak derivatives, Invariance of domain, The Riemann sphere is the published one-point compactification of the complex plane, The one-point (Alexandroff) compactification $X^{*} = X \cup {\infty}$ , whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$ , The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[F12]

Complex conjugation preserves modulus (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F13]

A continuous real-valued function on a finite closed interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Proof

technique · differentiate the moving interval averages, bound their derivative matrix by adjacent-interval quasisymmetry, and use properness followed by reflection across the line

1.1F2F3F13givenalgebra

Put $a (x, y) : = y^{- 1} \int_{x}^{x + y} h (t) d t$ and $b (x, y) : = y^{- 1} \int_{x - y}^{x} h (t) d t$ , so $H = u + i v$ with $u = (a + b) / 2$ and $v = a - b$ . These ordinary Riemann integrals exist because $h$ is continuous on every finite interval by [F13]. For example, the numerator in the difference quotient for $a_{x}$ is $\int_{x + y}^{x + y + s} h (t) d t - \int_{x}^{x + s} h (t) d t$ ; dividing by $s$ and using continuity gives $h (x + y) - h (x)$ . The endpoint quotient for $a_{y}$ , followed by differentiating the factor $1 / y$ , gives $R = (h (x + y) - a) / y$ ; the same endpoint computation for $b$ gives $Q = (h (x) - h (x - y)) / y$ and $- S = b_{y} = (h (x - y) - b) / y$ . Thus $P : = a_{x} = (h (x + y) - h (x)) / y$ , $Q : = b_{x} = (h (x) - h (x - y)) / y$ , $R : = a_{y} = (h (x + y) - a) / y$ , and $S : = - b_{y} = (b - h (x - y)) / y$ . These partial derivatives are continuous for $y > 0$ , so [F3] makes $H$ $C^{1}$ on $H$ .

1.2givenF1algebra

The imaginary part has the symmetric form $v (x, y) = y^{- 1} \int_{0}^{y} (h (x + s) - h (x - s)) d s > 0$ , since $h$ is strictly increasing. As $(x, y) \to (x_{0}, 0)$ with $y ↓ 0$ , continuity of $h$ makes both interval averages $a (x, y)$ and $b (x, y)$ tend to $h (x_{0})$ ; hence $u \to h (x_{0})$ and $v \to 0$ . Thus $H$ maps $H$ into itself and has the asserted continuous boundary values.

2.1F4step 1.1algebra

From the formulas in step 1.1, $u_{x} = (P + Q) / 2$ , $u_{y} = (R - S) / 2$ , $v_{x} = P - Q$ , and $v_{y} = R + S$ . Strict monotonicity gives $P, Q > 0$ and the averages satisfy $h (x) < a (x, y) < h (x + y)$ and $h (x - y) < b (x, y) < h (x)$ , hence $R, S > 0$ . Therefore $J_{H} = u_{x} v_{y} - u_{y} v_{x} = P S + Q R > 0$ . Applying [F4] at each point proves the local-diffeomorphism clause.

2.2F1step 1.1givenalgebra

Adjacent equal intervals give $P / L \leq Q \leq L P$ . Also $R \leq P$ and $S \leq Q$ . In fact, $R = y^{- 2} \int_{x}^{x + y} (h (x + y) - h (t)) d t \geq [h (x + y) - h (x + y / 2)] / (2 y) \geq P / [2 (1 + L)]$ , since the two adjacent half-increments of $[x, x + y]$ have sum $y P$ and ratio at most $L$ . Similarly, $S = y^{- 2} \int_{x - y}^{x} (h (t) - h (x - y)) d t \geq [h (x - y / 2) - h (x - y)] / (2 y) \geq Q / [2 (1 + L)]$ . Thus, with $c : = 1 / [2 (1 + L)]$ and $m : = c / L = 1 / [2 L (1 + L)]$ , every one of $P, Q, R, S$ lies between $m P$ and $L P$ .

2.3F1step 1.2algebra

To prove growth at infinity, note that $u$ is the average of $h$ on $[x - y, x + y]$ and $v \geq \frac{1}{2} [h (x + y / 2) - h (x - y / 2)]$ . If $y \leq ∣ x ∣ / 2$ , that interval lies in one tail, so $u \geq h (x / 2)$ for $x > 0$ and $u \leq h (- ∣ x ∣ / 2)$ for $x < 0$ . If $y \geq x / 2$ and $x > 0$ , the symmetric interval contains $[3 x / 4, 5 x / 4]$ ; comparison across four adjacent intervals of length $x / 4$ gives $v \geq \frac{1}{2} [h (5 x / 4) - h (x)] \geq (2 L^{4})^{- 1} [h (x / 4) - h (0)]$ . If $y \geq ∣ x ∣ / 2$ and $x < 0$ , it contains $[5 x / 4, 3 x / 4]$ ; comparison across three adjacent intervals of length $∣ x ∣ / 4$ gives $v \geq \frac{1}{2} [h (3 x / 4) - h (x)] \geq (2 L^{3})^{- 1} [h (0) - h (x / 4)]$ . For every $A > 0$ , choose $X$ so these tail bounds force $∣ u ∣ > A$ in the first case and $v > A$ in the second whenever $∣ x ∣ > X$ . When $∣ x ∣ \leq X$ , choose $Y$ so large that $v \geq \frac{1}{2} [h (y / 2 - X) - h (X - y / 2)] > A$ for $y > Y$ . If $∣ x + i y ∣ > \sqrt{X^{2} + Y^{2}}$ , either $∣ x ∣ > X$ or $∣ x ∣ \leq X$ and $y > Y$ ; the preceding estimates then give $∣ H (x + i y) ∣ > A$ . Hence $∣ H (x + i y) ∣ \to \infty$ as $∣ x + i y ∣ \to \infty$ .

3.1F5step 2.1step 2.2algebra

The derivative formulas now imply $∣ u_{x} ∣, ∣ u_{y} ∣, ∣ v_{x} ∣ \leq L P$ and $∣ v_{y} ∣ \leq 2 L P$ , so $∥ D H ∥_{H S}^{2} \leq 7 L^{2} P^{2}$ . Moreover $P S \geq m P^{2}$ and $Q R \geq (P / L) c P = m P^{2}$ , whence $J_{H} \geq 2 m P^{2} \geq m P^{2}$ and $∥ D H ∥_{H S}^{2} \leq C (L) J_{H}$ for $C (L) = 7 L^{2} / m = 14 L^{3} (1 + L)$ . By [F5], $2 (∣ H_{z} ∣^{2} + ∣ H_{\overset{ˉ}{z}} ∣^{2}) = ∥ D H ∥_{H S}^{2}$ and $J_{H} = ∣ H_{z} ∣^{2} - ∣ H_{\overset{ˉ}{z}} ∣^{2}$ ; rearranging yields $∣ H_{\overset{ˉ}{z}} ∣^{2} \leq [(C (L) - 2) / (C (L) + 2)] ∣ H_{z} ∣^{2}$ , which is clause (c).

3.2F7F9F10step 1.2step 2.3

Let $E \subset H$ be compact and nonempty. By [F9], $∣ w ∣$ has a finite maximum $M$ on $E$ and $Im w$ has a positive minimum $δ$ there. Step 2.3 bounds $∣ z ∣$ on $H^{- 1} (E)$ ; choose $R$ larger than that bound. The continuous extension from step 1.2 is uniformly continuous on the compact rectangle $[- R, R] \times [0, R]$ by [F9] and [F10]; since its imaginary part is zero on the bottom edge, there is $0 < ϵ < R$ such that $H^{- 1} (E)$ contains no point with $0 < y < ϵ$ . Thus $H^{- 1} (E)$ lies in the compact rectangle $[- R, R] \times [ϵ, R]$ and is closed there, because $E$ is closed in $H$ and $H$ is continuous. By [F9] it is compact. The empty $E$ has empty preimage, so $H$ is proper as defined in [F7].

4.1F7F8step 2.1step 3.2

The map $H : H \to H$ is a proper $C^{1}$ local diffeomorphism by steps 2.1 and 3.2. By [F7] it is a covering map; the target $H$ is convex and hence simply connected by [F8], so [F8] makes this connected covering one-sheeted. Therefore $H$ is a homeomorphism onto $H$ .

5.1F5F6F9F10F11F12step 3.1step 4.1

On every compact rectangle contained in $H$ , $H$ and its continuous first derivatives are bounded by [F9], and the rectangle has finite measure by [F10]. Therefore these classical derivatives are locally square-integrable, and the classical-to-weak derivative interface in [F11] shows $H \in W_{l o c}^{1, 2}$ . With the homeomorphism from step 4.1 and the inequality from step 3.1, [F6] gives analytic $K (L)$ -quasiconformality on $H$ . The reflected lower-half-plane map has the same local boundedness and finite-measure property, and its Wirtinger derivatives are $\overline{H_{z} (\overset{ˉ}{z})}$ and $\overline{H_{\overset{ˉ}{z}} (\overset{ˉ}{z})}$ ; the same interface and [F12] give its local Sobolev regularity and the same bound.

6.1F6F11step 1.2step 2.3step 4.1step 5.1given

Paste the upper and reflected lower maps along their common boundary values $h$ . The pasted plane map is continuous and bijective: each open half-plane maps bijectively to itself and $h$ maps the real line bijectively to itself. Invariance of domain makes it a homeomorphism. Step 2.3 and $h (x) \to \pm \infty$ as $x \to \pm \infty$ show it tends to $\infty$ at infinity. A plane homeomorphism and its inverse carry compact sets to compact sets by continuity, so the one-point compactification description in [F11] extends both to continuous inverse sphere maps fixing $\infty$ . It is $K (L)$ -quasiconformal off $R \cup {\infty}$ by step 5.1; applying the smooth-line removability theorem [F6] gives the asserted global $K (L)$ -quasiconformal homeomorphism.

7.1givenalgebra∎

For $\tilde{h} (x) = λ h (x / λ) + b$ , the substitution $t = λ s$ in each integral shows directly that its extension is $\tilde{H} (z) = λ H (z / λ) + b$ .

Remarks

The source's word “smooth” cannot be kept for arbitrary quasisymmetric $h$ . The odd square-root map $h (t) = sgn (t) \sqrt{∣ t ∣}$ is $4$ -quasisymmetric: by positive homogeneity it suffices to compare adjacent unit intervals with common endpoint $s$ ; for $0 \leq s \leq 1$ their image increments are $A = \sqrt{s} + \sqrt{1 - s}$ and $B = \sqrt{s + 1} - \sqrt{s}$ , with $1 \leq A \leq \sqrt{2}$ and $\sqrt{2} - 1 \leq B \leq 1$ , while for $s \geq 1$ they are $A = 1 / (\sqrt{s} + \sqrt{s - 1})$ and $B = 1 / (\sqrt{s + 1} + \sqrt{s})$ , whose ratio in either order is at most $1 + \sqrt{2} < 4$ ; negative $s$ follows by odd symmetry. At $y = 1$ , $u_{x} (x, 1) = \frac{1}{2} (h (x + 1) - h (x - 1))$ is not differentiable at $x = 1$ , since for $x < 1$ it equals $\frac{1}{2} (\sqrt{x + 1} + \sqrt{1 - x})$ and its derivative tends to $- \infty$ as $x ↑ 1$ . Thus the extension need not be $C^{2}$ , although the $C^{1}$ regularity proved above holds.

Depends on

Used by

Dependency tree · two levels

178 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

Mikhail Lyubich, Conformal Geometry and Dynamics of Quadratic Polynomials, vol. I (book draft, Stony Brook) (standard reference, not scraped)