ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Piecewise-affine approximation of a measurable coefficient

Statement

Assume Countable Choice. Let $Ω \subseteq C$ be a complex domain, let $μ$ be a Beltrami coefficient on $Ω$ , and suppose $0 \leq k < 1$ and $∥ μ ∥_{\infty} \leq k$ . For $n \geq 1$ , let $Q_{n}$ be the half-open dyadic squares in $C ≅ R^{2}$ of side $h_{n} = 2^{- n}$ . Choose a measurable representative $μ_{0}$ of $μ$ and define its zero extension $\tilde{μ}$ to $C$ by $\tilde{μ} = μ_{0}$ on $Ω$ and $\tilde{μ} = 0$ off $Ω$ . For $Q \in Q_{n}$ put $c_{Q} : = \frac{1}{λ_{2} (Q)} \int_{Q} \tilde{μ} d λ_{2},$ and set $μ_{n} (x) : = c_{Q}$ for $x \in Ω \cap Q$ . Then:

(a) Each $μ_{n}$ is measurable and constant, hence affine, on every dyadic cell $Ω \cap Q$ , and $∥ μ_{n} ∥_{\infty} \leq k$ .

(b) $μ_{n} (x) \to μ_{0} (x)$ at every $x \in Ω$ that is a Lebesgue point of $\tilde{μ}$ . Consequently $μ_{n} \to μ$ almost everywhere on $Ω$ .

(c) For any sequence of countable, locally finite triangulations of $C$ whose mesh tends to zero, there are piecewise-constant coefficients $ν_{j}$ with $∥ ν_{j} ∥_{\infty} \leq k$ and $ν_{j} \to μ$ almost everywhere on $Ω$ . Assign to each triangle $T$ the average of $\tilde{μ}$ over the ball centered at its barycenter with radius $diam T$ , and use that value on its cell. Averaging over the triangles themselves also gives convergence when the triangulations are uniformly shape-regular.

Facts & Assumptions

Given: Countable Choice; a complex domain $Ω$ ; a Beltrami coefficient $μ$ on $Ω$ ; and $0 \leq k < 1$ with $∥ μ ∥_{\infty} \leq k$ .

[F1]

A Beltrami coefficient is a Lebesgue-measurable almost-everywhere class of complex functions with its essential-supremum norm; planar domains carry two-dimensional Lebesgue measure (Measurable Beltrami coefficients and measurable conformal structures).

[F2]

Lebesgue measurability is understood through the real-coordinate measurable-space structure, and a complex domain is open in the Euclidean plane (Borel measurable and Lebesgue measurable functions on $R^{n}$ , A complex domain is a nonempty connected open subset of $C$ ).

[F3]

Complex $L^{\infty}$ functions are a.e. classes with essential-supremum norm, and complex integration is defined by its real and imaginary parts (Complex Lp classes and Euclidean test-function conventions, The space $L^{p} (μ)$ as the quotient by null functions).

[F4]

Every Euclidean ball has positive finite Lebesgue measure (Euclidean balls have positive finite Lebesgue measure).

[F5]

For complex $f \in L^{\infty}$ and $g \in L^{1}$ , $\int ∣ f g ∣ \leq ∥ f ∥_{\infty} ∥ g ∥_{1}$ and $∣ \int f g ∣ \leq ∥ f ∥_{\infty} ∥ g ∥_{1}$ (Complex Holder, Minkowski, and the quotient norm).

[F6]

A half-open square of side $h$ is measurable with measure $h^{2}$ ; a square of side $s$ has measure $s^{2}$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F7]

A.e.-equal integrable functions have equal integrals on every measurable set (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

[F8]

The ball average is $A_{r} f (x) = λ_{2} (B (x, r))^{- 1} \int_{B (x, r)} f$ , and a Lebesgue point is where the averages of $∣ f (y) - f (x) ∣$ tend to zero (The average of a locally integrable function over a Euclidean ball, Lebesgue points and the Lebesgue set of an $L_{l o c}^{1}$ class).

[F9]

Almost every point of a locally integrable function is a Lebesgue point (Almost every point is a Lebesgue point of a locally integrable function).

[F10]

A measurable complex function is locally integrable when its absolute value has finite integral on every ball (A locally integrable function on $R^{n}$ ).

[F11]

Countable Choice states that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Choice use. Countable Choice is assumed by the coefficient, measurable-function, Lebesgue-measure, and Lebesgue-point interfaces [F1], [F2], [F9], [F11]. Choosing one representative of the single given a.e. class is ordinary existential instantiation, and the averages are independent of that representative by [F7]. No full Axiom of Choice is used.

Proof

technique · direct

1.1F1F2F3F4F5F10given

Choose a measurable representative $μ_{0}$ of the given a.e. class and extend it by zero off $Ω$ , obtaining $\tilde{μ}$ . Since $Ω$ is open and hence Borel, [F2] makes the extension measurable. It satisfies $∥ \tilde{μ} ∥_{\infty} = ∥ μ ∥_{\infty} \leq k$ . For every ball $B$ , [F4] gives $1_{B} \in L^{1}$ with norm $λ_{2} (B) < \infty$ , and [F5] gives $\int_{B} ∣ \tilde{μ} ∣ \leq k λ_{2} (B)$ . Thus $\tilde{μ} \in L_{l o c}^{1} (R^{2})$ by [F10].

2.1F2F3F5F6F7step 1.1

Write $h_{n} = 2^{- n}$ . Each $Q \in Q_{n}$ has $λ_{2} (Q) = h_{n}^{2} > 0$ by [F6], so its average $c_{Q}$ is defined. A.e. changes of $μ_{0}$ do not change any $c_{Q}$ by [F7]. The half-open squares form a countable measurable partition of $R^{2}$ , so on $Ω$ the function $μ_{n}$ is measurable and constant on each $Ω \cap Q$ . Moreover [F5] gives $∣ c_{Q} ∣ = \frac{1}{h_{n}^{2}} ∣ \int_{Q} \tilde{μ} ∣ \leq \frac{∥ \tilde{μ} ∥_{\infty} ∥ 1_{Q} ∥_{1}}{h_{n}^{2}} \leq k,$ hence $∥ μ_{n} ∥_{\infty} \leq k$ .

3.1F6F8F9F11step 1.1step 2.1

Let $x \in Ω$ be a Lebesgue point of $\tilde{μ}$ , and let $Q_{n} (x)$ be its unique half-open dyadic square. Every point of $Q_{n} (x)$ is within distance $\sqrt{2} h_{n}$ of $x$ , so $Q_{n} (x) \subset B (x, \sqrt{2} h_{n})$ . The containing square of side $2 \sqrt{2} h_{n}$ has area $8 h_{n}^{2}$ by [F6], whence $λ_{2} (B (x, \sqrt{2} h_{n})) / h_{n}^{2} \leq 8$ . Therefore, writing $g_{x} (y) = ∣ \tilde{μ} (y) - \tilde{μ} (x) ∣$ , $∣ μ_{n} (x) - \tilde{μ} (x) ∣ \leq \frac{1}{h_{n}^{2}} \int_{Q_{n} (x)} g_{x} \leq 8 A_{\sqrt{2} h_{n}} g_{x} (x) ⟶ 0$ by [F8]. The Lebesgue points of $\tilde{μ}$ have full measure by [F9], proving (b) on $Ω$ .

4.1F2F3F4F5F6F8step 1.1step 3.1given

For a countable locally finite triangulation $T_{j}$ with mesh $δ_{j} \to 0$ , fix an enumeration of its triangles and assign shared faces to the first incident cell, giving a Borel partition. For a triangle $T$ , write $d_{T} = diam T > 0$ , let $c_{T}$ be its barycenter, and assign the constant $a_{T} : = \frac{1}{λ_{2} (B (c_{T}, d_{T}))} \int_{B (c_{T}, d_{T})} \tilde{μ}$ to its cell in $Ω$ . The resulting function is measurable by [F2]. If $x$ belongs to that cell, then $∣ x - c_{T} ∣ \leq d_{T}$ , so $B (c_{T}, d_{T}) \subset B (x, 2 d_{T})$ . The inner ball contains a square of side $\sqrt{2} d_{T}$ and the outer ball lies in a square of side $4 d_{T}$ ; [F4] and [F6] therefore give $\frac{λ_{2} (B (x, 2 d_{T}))}{λ_{2} (B (c_{T}, d_{T}))} \leq \frac{16 d_{T}^{2}}{2 d_{T}^{2}} = 8.$ Thus at every Lebesgue point $x$ the same estimate as in step 3.1 gives $∣ a_{T} - \tilde{μ} (x) ∣ \leq 8 A_{2 d_{T}} g_{x} (x)$ , which tends to zero uniformly as $d_{T} \leq δ_{j} \to 0$ . The averages remain bounded by $k$ by [F5]. If averages over $T$ itself are used and $λ_{2} (T) \geq c (diam T)^{2}$ uniformly, then $T \subset B (x, 2 d_{T})$ and the outer-to-cell measure ratio is at most $16 / c$ , giving the analogous estimate; this is the uniform shape-regularity condition stated in (c).

5.1step 2.1step 3.1step 4.1∎

Steps 2.1 and 3.1 prove (a) and (b), and step 4.1 proves the shape-independent triangulation version of (c).

Source notes

Lyubich §14.5 Exercise 14.3 asks for approximation of measurable coefficients by real-analytic ones, first via continuous coefficients, but does not supply the proof. Bishop Ch. 3 §1 computes the affine map between two labelled triangles; §2 states a continuous-coefficient mapping theorem, but its printed proof is blank. The proof here is supplied directly by zero extension, boundedness, and the Lebesgue-point theorem. The triangle version uses ball averages so its comparison is uniform without a shape assumption; cell averages themselves require shape regularity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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)
Christopher J. Bishop, Quasiconformal Mappings (Stony Brook Math 627 course notes, 164 pp.) (standard reference, not scraped)