Alphabeta Math
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.

Circular dilatation, quasisymmetry and the analytic definition

Sources

  • Mikhail Lyubich, Conformal Geometry and Dynamics of Quadratic Polynomials, vol. I, Ch. 2 §§12.2–12.5, printed pp. 185–188. Lemma 12.6 bounds the macroscopic circular dilatation of an analytic QC map by the annular modulus inequality; Proposition 12.7 records that bound. Lemma 12.11 and Proposition 12.13 give compact-set and normalized quasisymmetry. Proposition 12.14 gives an ACL* argument from bounded upper circular dilatation. Its p. 188 statement omits orientation preservation, although §12.5 defines quasiconformality for orientation-preserving homeomorphisms; the reflection h(z)=zˉ has circular dilatation 1 but fails the library's analytic Beltrami inequality, so part (iii) includes the orientation hypothesis explicitly.
  • The same volume, Ch. 2 §11.4, printed pp. 181–182, Proposition 11.14, gives the Jacobian-area estimates; §11.5, printed p. 183, states Proposition 11.18 for total differentiability but labels its proof as Project 11.19, “Fill in details.” The cited project is not used as a proof: the earlier quadrilateral core independently supplies total differentiability.
  • Christopher J. Bishop, Quasiconformal Mappings, Ch. 3 §4, printed pp. 91–96, for ACL, differentiability, and the Jacobian area estimates. The proof of Theorem 4.2 is not used as certified evidence here; its maximum argument is an open source obligation.

Statement

Assume the Axiom of Choice. Let h:U→V be a homeomorphism between plane domains. For z∈U and r>0 with D(z,r)‾⊂U, set Mh(z,r)=max⁡∣w−z∣=r∣h(w)−h(z)∣,mh(z,r)=min⁡∣w−z∣=r∣h(w)−h(z)∣, and define the macroscopic circular dilatation Dil⁡(h,z,r)=Mh(z,r)mh(z,r),Dil⁡(h,z)=lim sup⁡r↓0Dil⁡(h,z,r),Dil⁡(h)=sup⁡z∈UDil⁡(h,z).

(i) If h is analytically K-quasiconformal, then Dil⁡(h)≤eCK for an absolute constant C. More precisely, for every z∈U there is r0(z)>0 such that whenever 0<r<r0(z) and D(z,r)‾⊂U, the inner and outer radii s,R of h(D(z,r)) about h(z) satisfy log⁡(R/s)≤CK.

(ii) If Dil⁡(h)<∞, then h is quasisymmetric on compact subsets, with control depending on Dil⁡(h) and the relative distances of the compact set and its image from the domain boundaries. In particular, a K-quasiconformal homeomorphism is locally quasisymmetric with control depending only on K and these distances, and its inverse has the corresponding inverse control function.

(iii) If h is orientation-preserving and Dil⁡(h)≤L<∞, then h is analytically L-quasiconformal: it is ACL on almost every horizontal and vertical line, belongs to Wloc1,2, is differentiable almost everywhere, and satisfies ∣hzˉ∣≤L−1L+1∣hz∣a.e.

The metric assertions (i) and (ii) do not need an added orientation premise; the analytic conclusion (iii) requires orientation preservation, since complex conjugation has circular dilatation one. The constants in (i) and (ii) are not sharp; the Beltrami constant in (iii) follows from the pointwise differential eccentricity bound.

Facts & Assumptions

Given: The Axiom of Choice, plane domains U,V, the homeomorphism h, and the circular dilatations in the Statement. Part (iii) also assumes the orientation-preserving condition of Orientation-preserving homeomorphisms and the geometric definition of quasiconformality.

[F1]

At a differentiability point with nonsingular derivative, the limsup circular ratio equals the derivative singular-value ratio. A rank-one derivative forces that ratio to infinity by testing kernel and transverse directions, while a zero derivative already satisfies the Beltrami inequality. Thus once the necessary ACL/weak regularity is established, the sharp analytic L bound follows from the circular bound and the Wirtinger identities (The Wirtinger derivatives ∂zf and ∂zˉf, and antiholomorphic functions).

[F2]

The full earlier ring theorem gives both annular end-family distortion bounds (An analytically quasiconformal homeomorphism distorts quadrilateral moduli by at most K). The round-annulus value is λ(A(s,R))=(2π)−1log⁡(R/s) (Extremal length of the rectangle and of the round annulus). The continuum-circle argument below supplies the required absolute source-ring bound locally; no cited annulus-geometry lemma is used. The circle estimate uses completed-product Fubini and Jordan separation (Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, Jordan–Schönflies extension for plane curves, Jordan–Brouwer separation).

[F3]

A map is η-quasisymmetric when ∣x−a∣≤t∣x−b∣ implies ∣h(x)−h(a)∣≤η(t)∣h(x)−h(b)∣ for distinct triples, where η:[0,∞)→[0,∞) is an increasing homeomorphism with η(0)=0. Reversing this ratio inequality gives the inverse control η∗(t)=1/η−1(1/t) for t>0, with η∗(0)=0. Step 2.1 proves the local control needed here. Lyubich, §12.3, supplies the convention; Lemma 12.11 concerns embeddings of the whole Euclidean space with an all-scale circular bound, rather than this compact-set statement.

[F4]

The sole delegated citation input is qualitative: an orientation-preserving homeomorphism between finite planar domains with bounded upper infinitesimal circular dilatation everywhere is analytically quasiconformal with some finite constant. This is Gehring, Definitions for a Class of Plane Quasiconformal Mappings (1967), §9 Definition8′, printed p.179, with §3 Definitions2/2′, p.176 and the orientation/domain convention on p.175. The complete ten-page paper was read; §14 points elsewhere for the equivalence proof, so this is a statement citation under the exact root-recorded last-resort authorization, not a claim that this paper supplies that proof. The sharp L bound, area arguments, modulus comparison and quasisymmetry estimates below are local. Total differentiability after this qualitative regularity is the earlier independently proved core Remark (Analytic quasiconformality gives both quadrilateral modulus bounds).

Proof

technique · use only the authorized qualitative metric criterion, derive its sharp bound locally, and prove analytic circular/quasisymmetry control by continuum-circle modulus and dyadic shrink
1.1F1F4givenalgebra

Assume h preserves orientation and its upper circular dilatation is at most L everywhere. The exact qualitative citation [F4] gives ACL, local W1,2 and finite analytic distortion. The general differentiability argument in the core Remark applies, without assuming a sharp analytic constant. At every nonsingular differentiability point, [F1] identifies the circular limsup with the singular-value ratio, bounded by L. A rank-one derivative would force an infinite circular ratio and is excluded; rank zero satisfies the Beltrami inequality. Thus ∣hzˉ∣≤(L−1)(L+1)−1∣hz∣ a.e., and the already-obtained W1,2 regularity makes h analytically L-quasiconformal. This proves (iii); no sharp bound is obtained merely by citing [F4].

1.2F2givenconstructalgebra

Fix a source point x and a sufficiently small radius r so that the disk of outer radius R=Mh(x,r) about h(x) lies inside V; put s=mh(x,r). The preimage of the round ring centered at h(x) with radii s,R has inner Jordan continuum E containing x and a point at distance r from x, and outer closed Jordan exterior F containing a point at distance r and infinity. Thus diam(E) is at least r and d=dist⁡(E,F)≤2r. Choose a closest pair e0,f0 and its midpoint c. There is e in E with ∣e−e0∣≥r/2; a compact path in the Jordan exterior F from f0 toward infinity gives an analogous far point. Since the pair is closest, ∣e−f0∣≥d, whence ∣e−c∣2≥d2/4+∣e−e0∣2/2≥d2/4+r2/8, and likewise on F. Connectedness makes every circle centered at c with radius between d/2 and d2/4+r2/8 meet both continua. One complementary circle arc has one endpoint on each and lies inside the ring, so an admissible density has integral at least one on that whole circle. Cauchy–Schwarz and polar Fubini give source modulus at least 14πlog⁡(1+r2/(2d2))≥c0:=14πlog⁡(9/8)>0. If R=s the ratio is one and no ring is needed. Otherwise [F2] gives (2π)−1log⁡(R/s)≤K/c0. Thus R/s≤eCK with the absolute constant C=2π/c0. The closest pair exists because E is compact and F closed; the exterior path and circle-arc separation use Jordan–Schönflies. For a fixed compact source set, choose the small radii uniformly by continuity on a larger compact neighborhood and its positive image distance from the target boundary. This proves (i).

2.1F1F3step 1.1step 1.2givenconstructalgebra∎

For an analytic map, step 1.2 gives a uniform small-scale circular bound H on each compact neighborhood. Openness makes the maximum image distance in a closed source ball occur on its boundary. Put d=Lx(r/2) and choose y on that inner circle realizing d, with midpoint yprime of x,y. The equal-radius comparison at yprime gives d≤(H+1)∣h(y)−h(yprime)∣, and the comparison at y gives ∣h(y)−h(yprime)∣≤Hly(r/4). The image of B(y,r/4) contains the disk of its inner radius, is inside h(B(x,r)), and is centered a distance d from h(x). Hence Lx(r)≥(1+c)d with c=1/[H(H+1)]. Iteration gives Lx(tr)≤CHtαlx(r) for 0<t≤1, where α=log⁡2(1+c)>0. The reverse doubling bound is Lx(2r)≤(H+1)Lx(r): take a maximizing point at radius2r, its midpoint, and compare the two equal-radius increments about that midpoint. Iteration supplies an increasing power bound for t at least1. These give the local quasisymmetry control in the analytic case; finite compact collars extend the control over the compact set. The inverse control formula is η∗(t)=1/η−1(1/t) by reversing the ratio inequality. For a general bounded-circular map, apply step 1.1; when its orientation is reversed first postcompose with complex conjugation, which preserves every distance ratio and changes the orientation. The resulting analytic constant is L, so step 1.2 and the same shrink argument apply. On each compact collar the small-scale estimate handles triples of sufficiently small diameter; for the remaining triples the fixed positive minimum image separation completes a continuous control function. The input/output collar data enter this compact control. If the domains are the whole plane, step 1.2 has no small-radius restriction, and the shrink and doubling inequalities hold at all scales with control depending only on K. This proves the claimed local metric control and its inverse formula; the global-plane conclusion uses no domain-boundary data.

Remark

For an analytically K-quasiconformal homeomorphism of the whole plane, the continuum-circle proof has no boundary restriction. Put H=eCK, c=1/[H(H+1)], α=log⁡2(1+c) and β=log⁡2(H+1). The proved all-scale shrink and doubling inequalities give a global Euclidean quasisymmetry control η(t)=CHtα for 0≤t≤1 and η(t)=CHtβ for t≥1, with CH=Hmax⁡(1+c,H+1). This conclusion uses the local analytic modulus argument; the delegated citation is only the initial qualitative criterion for a general metric map.

Depends on

Used by

Dependency tree · two levels

198 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