Area and change of variables for a holomorphic map

Where its derivative does not vanish a holomorphic map is conformal: at such a point z it acts on the plane as a rotation followed by a dilation of ratio ‖deriv f z‖. At every point, critical or not, it multiplies infinitesimal area by ‖deriv f z‖ ^ 2. Integrating that pointwise distortion over a set on which f is injective gives the area formula, volume (f '' s) = ∫⁻ z in s, ‖deriv f z‖ₑ ^ 2, and its immediate corollary that a holomorphic injection whose image has finite area has a finite Dirichlet integral ∫⁻ z in s, ‖deriv f z‖ₑ ^ 2.

That finiteness is the analytic input of the length–area method, the classical route to layer L5 of the conformal-mapping roadmap (ConformalMapping/README.md), Carathéodory's boundary correspondence: for a conformal map of the disc onto a bounded domain, the finite Dirichlet integral is spent along the circular arcs {z ∈ ball 0 1 | ‖z - ζ‖ = ρ} approaching a boundary point ζ, so by Cauchy–Schwarz the images of those arcs must be short for some arbitrarily small ρ, which is what forces the boundary cluster set at ζ to degenerate to a point. The topological half of that argument is already on main: TauCeti.exists_continuousOn_closure_eqOn turns a subsingleton cluster set into a continuous extension. The analytic half, of which the area formula is the first component, is not; the degeneracy itself is not proved here.

Weighting that same distortion by an arbitrary integrand generalises the area formula to the change of variables formula for a holomorphic injection, ∫⁻ w in f '' s, g w = ∫⁻ z in s, ‖deriv f z‖ₑ ^ 2 * g (f z), of which the area formula is the case g = 1. (The area formula is nevertheless kept separate: it holds for a merely null measurable s, while the weight forces the measurability that Mathlib's change of variables asks for.) The integrability and Bochner forms generalise TauCeti.integrableOn_norm_deriv_sq and TauCeti.integral_norm_deriv_sq_eq_toReal_volume_image the same way, and are stated for an integrand valued in an arbitrary real normed space, as Mathlib's are.

The proof is Mathlib's change-of-variables formula MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀ for an injective differentiable map, applied to f viewed as a map of the real plane. The only complex-analytic input is the value of the Jacobian determinant: the ℝ-linear map underlying multiplication by c : ℂ has determinant Complex.normSq c = ‖c‖ ^ 2, which is the private det_restrictScalars_smulRight_one below and comes from Algebra.norm_complex_eq through LinearMap.det_restrictScalars. Injectivity is what makes the formula an equality rather than the inequality TauCeti.volume_image_le_lintegral_enorm_deriv_sq, which holds for any holomorphic map because a non-injective map covers parts of its image more than once.

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0–L6, the results below are stated for maps of ℂ. The hypotheses are the roadmap's: an open domain U, DifferentiableOn ℂ f U, and Set.InjOn. Statements are made for an arbitrary s ⊆ U rather than for U itself, because the length–area argument integrates over the sub-annuli U ∩ {z | ρ₁ < ‖z - ζ‖ < ρ₂}, not over U; take s = U with hUo.measurableSet and subset_rfl for the plain domain form. The area formula and the finiteness it gives ask only for MeasureTheory.NullMeasurableSet s volume, as Mathlib's null-measurable change of variables does; every other statement below asks for MeasurableSet s — the Bochner-integral forms because that is what turns the continuity of deriv f into strong measurability on s, and all three weighted change-of-variables forms because that is what Mathlib's weighted change of variables asks for.

Main results

• TauCeti.volume_image_eq_lintegral_enorm_deriv_sq — the area formula: the area of the image of a set on which a holomorphic map is injective is the integral of ‖deriv f‖ ^ 2 over it.
• TauCeti.volume_image_le_lintegral_enorm_deriv_sq — the inequality form, with no injectivity.
• TauCeti.lintegral_enorm_deriv_sq_ne_top and TauCeti.integrableOn_norm_deriv_sq — a holomorphic injection whose image has finite area has a finite Dirichlet integral; TauCeti.lintegral_enorm_deriv_sq_ne_top_of_isBounded and TauCeti.integrableOn_norm_deriv_sq_of_isBounded are the forms taking a bounded image.
• TauCeti.integral_norm_deriv_sq_eq_toReal_volume_image — the Bochner-integral form of the area formula.
• TauCeti.volume_image_eq_zero_iff — a holomorphic injection whose derivative is almost everywhere nonzero carries null sets to null sets and back.
• TauCeti.lintegral_enorm_deriv_sq_eq_pi_of_image_eq_ball — the Dirichlet integral of a Riemann map is exactly π.
• TauCeti.lintegral_image_eq_lintegral_enorm_deriv_sq_mul, TauCeti.integrableOn_image_iff_integrableOn_norm_deriv_sq_smul and TauCeti.integral_image_eq_integral_norm_deriv_sq_smul — the change of variables formula for a holomorphic injection, in Lebesgue, integrability and Bochner form.

Coordination with upstream Mathlib

Mathlib has the change-of-variables formula but no area formula for holomorphic maps: a grep of the pinned Mathlib for lintegral_abs_det_fderiv finds only the polar-coordinate and upper-half-plane applications, neither of which computes the area of a conformal image. Layer L5 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which stops at the mapping theorem itself, so this file is new Lean formalization rather than a temporary shim.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, §2.2 (the length–area method).
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX.
• P. L. Duren, Univalent Functions, Ch. 2 (the area theorem).

theorem TauCeti.volume_image_eq_lintegral_enorm_deriv_sq {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hsU : s ⊆ U) (hinj : Set.InjOn f s) : MeasureTheory.volume (f '' s) = ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2

The area formula. If f is holomorphic on an open set U and injective on a null measurable s ⊆ U, then the area of f '' s is the integral over s of the area distortion ‖deriv f z‖ ^ 2.

Injectivity is essential: without it the map covers part of its image more than once and only the inequality TauCeti.volume_image_le_lintegral_enorm_deriv_sq survives.

theorem TauCeti.volume_image_le_lintegral_enorm_deriv_sq {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) : MeasureTheory.volume (f '' s) ≤ ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2

The area inequality for a holomorphic map. Dropping injectivity from the area formula leaves an inequality, since a map that covers a part of its image several times spends more of the integral ∫⁻ z in s, ‖deriv f z‖ₑ ^ 2 than the area of the image accounts for.

theorem TauCeti.lintegral_enorm_deriv_sq_ne_top {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (hfin : MeasureTheory.volume (f '' s) ≠ ⊤) : ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2 ≠ ⊤

A holomorphic injection whose image has finite area has a finite Dirichlet integral. This is the finiteness that the length–area method spends: the whole of ∫⁻ z in s, ‖deriv f z‖ₑ ^ 2 is available to bound the lengths of the images of the circular arcs approaching a boundary point, so all but finitely much of it must be spread thinly.

theorem TauCeti.lintegral_enorm_deriv_sq_ne_top_of_isBounded {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (hb : Bornology.IsBounded (f '' s)) : ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2 ≠ ⊤

The bounded-image form of TauCeti.lintegral_enorm_deriv_sq_ne_top: a holomorphic injection with bounded image has a finite Dirichlet integral.

theorem TauCeti.integrableOn_norm_deriv_sq {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (hfin : MeasureTheory.volume (f '' s) ≠ ⊤) : MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖deriv f z‖ ^ 2) s MeasureTheory.volume

The Bochner-integrability form of TauCeti.lintegral_enorm_deriv_sq_ne_top: the area distortion of a holomorphic injection whose image has finite area is integrable. Measurability is free because the derivative of a holomorphic function is again holomorphic, hence continuous.

theorem TauCeti.integrableOn_norm_deriv_sq_of_isBounded {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (hb : Bornology.IsBounded (f '' s)) : MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖deriv f z‖ ^ 2) s MeasureTheory.volume

The bounded-image form of TauCeti.integrableOn_norm_deriv_sq: the area distortion of a holomorphic injection with bounded image is integrable.

theorem TauCeti.integral_norm_deriv_sq_eq_toReal_volume_image {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) : ∫ (z : ℂ) in s, ‖deriv f z‖ ^ 2 = (MeasureTheory.volume (f '' s)).toReal

The area formula, Bochner form. The area of the image of a holomorphic injection is the ordinary integral of the area distortion.

No finiteness is needed: if the area distortion is not integrable then both sides are 0, the Bochner integral by convention and the right-hand side because (⊤ : ℝ≥0∞).toReal = 0.

theorem TauCeti.volume_image_eq_zero_iff {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (hd : ∀ᵐ (z : ℂ) ∂MeasureTheory.volume.restrict s, deriv f z ≠ 0) : MeasureTheory.volume (f '' s) = 0 ↔ MeasureTheory.volume s = 0

A holomorphic injection carries null sets to null sets and back. Where the derivative is almost everywhere nonzero, the image of a measurable set is null exactly when the set is.

The nonvanishing is not an extra assumption in the intended case s = U: a holomorphic map injective on the open set U has nonvanishing derivative throughout U, by TauCeti.not_injOn_of_deriv_eq_zero, so MeasureTheory.ae_restrict_of_forall_mem supplies hd. It is kept as a hypothesis so that the statement also covers a proper subset s, which need not be a neighbourhood of its points.

Only the forward implication needs the derivative: a differentiable map carries null sets to null sets whatever its derivative does, whereas a set of positive measure has a null image only if the area distortion ‖deriv f‖ ^ 2 vanishes on much of it.

theorem TauCeti.lintegral_enorm_deriv_sq_eq_pi_of_image_eq_ball {U : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hinj : Set.InjOn f U) (himg : f '' U = Metric.ball 0 1) : ∫⁻ (z : ℂ) in U, ‖deriv f z‖ₑ ^ 2 = ENNReal.ofReal Real.pi

The Dirichlet integral of a Riemann map is π. A holomorphic injection of an open set onto the unit disc spends exactly the area of the disc.

The hypotheses are those of the conclusion of the Riemann mapping theorem TauCeti.riemannMapping, so the statement is not vacuous: every nonempty simply connected proper open subset of ℂ carries such an f.

The change of variables formula

theorem TauCeti.lintegral_image_eq_lintegral_enorm_deriv_sq_mul {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (g : ℂ → ENNReal) : ∫⁻ (w : ℂ) in f '' s, g w = ∫⁻ (z : ℂ) in s, ‖deriv f z‖ₑ ^ 2 * g (f z)

The change of variables formula for a holomorphic injection. Integrating over the image f '' s is the same as integrating the pulled-back integrand against the area distortion ‖deriv f z‖ ^ 2 over s.

Taking g = 1 recovers TauCeti.volume_image_eq_lintegral_enorm_deriv_sq; that statement is not deduced from this one, because it needs s only null measurable, while the weight forces the measurability that Mathlib's MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul asks for.

theorem TauCeti.integrableOn_image_iff_integrableOn_norm_deriv_sq_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (g : ℂ → E) : MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖deriv f z‖ ^ 2 • g (f z)) s MeasureTheory.volume

Integrability under the change of variables formula. A function is integrable on the image of a holomorphic injection exactly when its pullback, weighted by the area distortion, is integrable on the source.

This is what makes TauCeti.integral_image_eq_integral_norm_deriv_sq_smul more than a statement about the junk value 0 that the Bochner integral takes on non-integrable functions.

theorem TauCeti.integral_image_eq_integral_norm_deriv_sq_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {U s : Set ℂ} {f : ℂ → ℂ} (hUo : IsOpen U) (hf : DifferentiableOn ℂ f U) (hs : MeasurableSet s) (hsU : s ⊆ U) (hinj : Set.InjOn f s) (g : ℂ → E) : ∫ (w : ℂ) in f '' s, g w = ∫ (z : ℂ) in s, ‖deriv f z‖ ^ 2 • g (f z)

The change of variables formula, Bochner form.

No integrability hypothesis is needed: if either side fails to be integrable then so does the other, by TauCeti.integrableOn_image_iff_integrableOn_norm_deriv_sq_smul, and both Bochner integrals are 0.