The lower integral of a weight over a circle, and the length–area inequality

For a weight g : ℂ → ℝ≥0∞ this file introduces TauCeti.circleLIntegral g ζ ρ, the lower integral of g over the circle of centre ζ and radius ρ with respect to arc length, computed through Mathlib's parametrisation circleMap ζ ρ, which for ρ > 0 runs once around that circle at the constant speed ρ:

circleLIntegral g ζ ρ = ENNReal.ofReal ρ * ∫⁻ θ in Ioo (-π) π, g (circleMap ζ ρ θ).

For ρ ≤ 0 the factor ENNReal.ofReal ρ makes the value 0, a convention rather than a reading of the parametrisation; the arc-length statements below are therefore statements about ρ > 0.

Two facts about it are proved, and they are the two halves of the classical length–area method.

The first is polar Fubini: integrating the circle integrals over all radii recovers the plane integral,

∫⁻ ρ in Ioi 0, circleLIntegral g ζ ρ = ∫⁻ z, g z

(TauCeti.lintegral_circleLIntegral_eq_lintegral), for every measurable g and every centre ζ. This is Mathlib's Complex.lintegral_comp_polarCoord_symm recentred at ζ and unfolded into an iterated integral, the factor ENNReal.ofReal ρ in the definition being exactly the Jacobian ρ dρ dθ of polar coordinates.

The second is Cauchy–Schwarz on the circle: the square of the circle integral of g is at most 2 π ρ — for ρ > 0 the length of the circle — times the circle integral of g ^ 2 (TauCeti.circleLIntegral_sq_le). Dividing by ρ and integrating in ρ, polar Fubini reassembles the right-hand side into the plane integral of g ^ 2 and gives the length–area inequality

∫⁻ ρ in Ioi 0, circleLIntegral g ζ ρ ^ 2 / ρ ≤ 2 π ∫⁻ z, g z ^ 2

(TauCeti.lintegral_circleLIntegral_sq_div_le_lintegral_sq). Since the logarithmic measure ∫⁻ ρ in Ioo r R, ρ⁻¹ = log (R / r) of an annulus diverges as r → 0, a finite right-hand side cannot keep circleLIntegral g ζ ρ ^ 2 above a positive constant throughout a long annulus: Wolff's lemma TauCeti.exists_circleLIntegral_sq_lt produces a radius ρ between r and R with circleLIntegral g ζ ρ ^ 2 < c as soon as 2 π ∫⁻ z, g z ^ 2 < c * log (R / r).

The threshold 2 π ∫⁻ z, g z ^ 2 / log (R / r) that lemma asks to be beaten falls to 0 as the annulus is made longer, so for a weight of finite square integral it is beaten by every positive c once the annulus is long enough. Shrinking the annulus onto the centre — take the outer radius R as given and the inner one R * exp (-L) with L large — that is TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top: below every bound R there is a radius ρ with circleLIntegral g ζ ρ smaller than any prescribed c ≠ 0. Equivalently, and sharply, the circle integral has lower limit zero at the centre, TauCeti.liminf_circleLIntegral_nhdsGT_eq_zero. Only a lower limit is available, and that is not a defect of the proof: the weight ‖z - ζ‖⁻¹ / (2 π) cut down to a sequence of thin annuli Ioo aₙ (aₙ * (1 + εₙ)) with ∑ εₙ finite has finite square integral yet circle integral 1 at every radius in those annuli, so circleLIntegral g ζ ρ need not tend to 0 as ρ → 0.

Nothing here is analytic: g is an arbitrary measurable weight, and the two inputs are the polar-coordinate change of variables and Hölder's inequality. The analytic use is TauCeti/Analysis/Complex/Conformal/LengthArea.lean, which takes g to be ‖deriv f‖ₑ cut off outside a set s, so that circleLIntegral g ζ ρ becomes the arc length of the image of a circular arc under a holomorphic f and ∫⁻ z, g z ^ 2 its Dirichlet integral, hence the area of the image; that file is the layer L5 input of TauCetiRoadmap/ConformalMapping/README.md. Stating the estimates for a weight keeps them available to any other length-versus-area argument — the plane integral on the right need not be an area and the circle integral on the left need not be a length.

Main definitions and results

• TauCeti.circleLIntegral — the lower integral of a weight over a circle with respect to arc length, through the parametrisation circleMap.
• TauCeti.circleLIntegral_eq_lintegral_Ioc — the angular integral may be taken over any period, so the branch cut at ±π fixed in the definition is immaterial.
• TauCeti.lintegral_circleLIntegral_eq_lintegral — polar Fubini: the circle integrals about any centre integrate over the radii to the plane integral.
• TauCeti.circleLIntegral_sq_le — Cauchy–Schwarz on the circle: the square of the circle integral of g is at most the circumference times the circle integral of g ^ 2.
• TauCeti.lintegral_circleLIntegral_sq_div_le_lintegral_sq — the length–area inequality.
• TauCeti.exists_circleLIntegral_sq_lt — Wolff's lemma: a radius with small circle integral exists in every annulus whose logarithmic measure is large enough.
• TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top — its limiting form for a weight of finite square integral: below every positive bound there is a radius at which the circle integral is smaller than any prescribed c ≠ 0.
• TauCeti.liminf_circleLIntegral_nhdsGT_eq_zero — the same statement as a lower limit: the circle integrals of a weight of finite square integral have lower limit 0 at the centre.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, §2.2 (the length–area method).
• P. L. Duren, Univalent Functions, Ch. 3.

The circle integral of a weight

noncomputable def TauCeti.circleLIntegral (g : ℂ → ENNReal) (ζ : ℂ) (ρ : ℝ) : ENNReal

The lower integral of the weight g over the circle of centre ζ and radius ρ, taken with respect to arc length: for ρ > 0, the angular integral of g ∘ circleMap ζ ρ scaled by the speed ρ of that parametrisation.

Nothing is assumed of g, so this is a lower integral of a possibly non-measurable integrand. The angle runs over Ioo (-π) π, one full period of circleMap ζ ρ; by TauCeti.circleLIntegral_eq_lintegral_Ioc any other period gives the same value. A nonpositive radius gives the value 0, by the factor ENNReal.ofReal ρ: that is a deliberate convention, not a property of the parametrisation, since for ρ < 0 the map circleMap ζ ρ still runs once around the circle of radius |ρ|, at speed |ρ| and in the same direction, only rotated by π.

Equations

• TauCeti.circleLIntegral g ζ ρ = ENNReal.ofReal ρ * ∫⁻ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, g (circleMap ζ ρ θ)

theorem TauCeti.circleLIntegral_def (g : ℂ → ENNReal) (ζ : ℂ) (ρ : ℝ) : circleLIntegral g ζ ρ = ENNReal.ofReal ρ * ∫⁻ (θ : ℝ) in Set.Ioo (-Real.pi) Real.pi, g (circleMap ζ ρ θ)

The defining angular integral. The body of TauCeti.circleLIntegral is not @[expose]d, so this is the form in which other modules reach the definition.

theorem TauCeti.circleLIntegral_mono_on {g h : ℂ → ENNReal} (ζ : ℂ) (ρ : ℝ) (hgh : 0 < ρ → ∀ z ∈ Metric.sphere ζ ρ, g z ≤ h z) : circleLIntegral g ζ ρ ≤ circleLIntegral h ζ ρ

Increasing the weight on the circle increases its circle integral: only the values on Metric.sphere ζ ρ, the circle the integral is taken over, matter.

The comparison is asked for only at a positive radius, since at a nonpositive one both sides are 0 and nothing about g and h is needed.

theorem TauCeti.circleLIntegral_congr {g h : ℂ → ENNReal} (ζ : ℂ) (ρ : ℝ) (hgh : 0 < ρ → Set.EqOn g h (Metric.sphere ζ ρ)) : circleLIntegral g ζ ρ = circleLIntegral h ζ ρ

Weights agreeing on the circle have the same circle integral; as in TauCeti.circleLIntegral_mono_on, agreement is asked for only at a positive radius.

@[simp]

theorem TauCeti.circleLIntegral_const (a : ENNReal) (ζ : ℂ) (ρ : ℝ) : circleLIntegral (fun (x : ℂ) => a) ζ ρ = ENNReal.ofReal (2 * Real.pi * ρ) * a

The circle integral of a constant weight is 2 π ρ — for ρ > 0 the circumference of the circle — times that constant; for ρ ≤ 0 both sides are 0.

@[simp]

theorem TauCeti.circleLIntegral_of_nonpos {ρ : ℝ} (g : ℂ → ENNReal) (ζ : ℂ) (hρ : ρ ≤ 0) : circleLIntegral g ζ ρ = 0

The circle integral vanishes at a nonpositive radius, by the factor ENNReal.ofReal ρ in the definition of TauCeti.circleLIntegral. This is that convention, not a geometric statement: for ρ < 0 the parametrisation circleMap ζ ρ still runs once around the circle of radius |ρ|.

@[simp]

theorem TauCeti.circleLIntegral_zero (ζ : ℂ) (ρ : ℝ) : circleLIntegral 0 ζ ρ = 0

The zero weight has zero circle integral.

theorem TauCeti.circleLIntegral_add {g h : ℂ → ENNReal} (ζ : ℂ) (ρ : ℝ) (hg : AEMeasurable (fun (θ : ℝ) => g (circleMap ζ ρ θ)) (MeasureTheory.volume.restrict (Set.Ioo (-Real.pi) Real.pi))) : circleLIntegral (fun (z : ℂ) => g z + h z) ζ ρ = circleLIntegral g ζ ρ + circleLIntegral h ζ ρ

The circle integral is additive in the weight, as soon as one summand has an a.e. measurable angular trace along the circle at hand; as in TauCeti.circleLIntegral_sq_le, nothing is assumed of either weight off that circle. Some such hypothesis is needed, a lower integral being only superadditive in general. It is the hypothesis of MeasureTheory.lintegral_add_left', which is why — like that lemma, and unlike its Measurable counterpart — this is not a simp lemma.

theorem TauCeti.circleLIntegral_const_mul (a : ENNReal) (g : ℂ → ENNReal) (ζ : ℂ) (ρ : ℝ) (ha : a ≠ ⊤) : circleLIntegral (fun (z : ℂ) => a * g z) ζ ρ = a * circleLIntegral g ζ ρ

A finite constant comes out of the circle integral. This is MeasureTheory.lintegral_const_mul', whose finiteness hypothesis on the constant is what lets the weight stay arbitrary; as there, no measurability is needed.

theorem TauCeti.circleLIntegral_eq_lintegral_Ioc (g : ℂ → ENNReal) (ζ : ℂ) (ρ t : ℝ) : circleLIntegral g ζ ρ = ENNReal.ofReal ρ * ∫⁻ (θ : ℝ) in Set.Ioc t (t + 2 * Real.pi), g (circleMap ζ ρ θ)

The angular integral may be taken over any period. The interval Ioo (-π) π fixed in the definition of TauCeti.circleLIntegral can be replaced by any Ioc t (t + 2 * π), so nothing about the quantity depends on the branch cut at ±π; in particular an arc of the circle that crosses the seam is handled by choosing t beyond its far endpoint.

Polar Fubini

theorem TauCeti.lintegral_circleLIntegral_eq_lintegral {g : ℂ → ENNReal} (hg : Measurable g) (ζ : ℂ) : ∫⁻ (ρ : ℝ) in Set.Ioi 0, circleLIntegral g ζ ρ = ∫⁻ (z : ℂ), g z

Polar Fubini for the lower integral. Integrating the circle integrals of a measurable weight over all radii recovers its plane integral, whatever centre the circles are taken about.

This is the polar-coordinate change of variables Complex.lintegral_comp_polarCoord_symm, recentred at ζ by translation invariance of the plane measure and unfolded into an iterated integral over the radius and the angle; the factor ENNReal.ofReal ρ built into TauCeti.circleLIntegral is the Jacobian.

Cauchy–Schwarz on a circle, and the length–area inequality

theorem TauCeti.circleLIntegral_sq_le {g : ℂ → ENNReal} (ζ : ℂ) (ρ : ℝ) (hg : AEMeasurable (fun (θ : ℝ) => g (circleMap ζ ρ θ)) (MeasureTheory.volume.restrict (Set.Ioo (-Real.pi) Real.pi))) : circleLIntegral g ζ ρ ^ 2 ≤ ENNReal.ofReal (2 * Real.pi * ρ) * circleLIntegral (fun (z : ℂ) => g z ^ 2) ζ ρ

Cauchy–Schwarz on a circle. The square of the circle integral of g is at most 2 π ρ — for ρ > 0 the circumference of the circle — times the circle integral of g ^ 2.

Only the angular trace of g along the circle at hand need be measurable; nothing is assumed of g off that circle. Both sides vanish for a nonpositive radius, so no positivity is assumed.

theorem TauCeti.lintegral_circleLIntegral_sq_div_le_lintegral_sq {g : ℂ → ENNReal} (hg : Measurable g) (ζ : ℂ) : ∫⁻ (ρ : ℝ) in Set.Ioi 0, circleLIntegral g ζ ρ ^ 2 / ENNReal.ofReal ρ ≤ ENNReal.ofReal (2 * Real.pi) * ∫⁻ (z : ℂ), g z ^ 2

The length–area inequality. For a measurable weight g and any centre ζ, the integral over all radii of circleLIntegral g ζ ρ ^ 2 / ρ is at most 2 π times the plane integral of g ^ 2.

This is Cauchy–Schwarz on each circle (TauCeti.circleLIntegral_sq_le) — the source of the factor 2 π — followed by polar Fubini (TauCeti.lintegral_circleLIntegral_eq_lintegral) applied to the weight g ^ 2, which reassembles the circle integrals of g ^ 2 into its plane integral.

theorem TauCeti.exists_circleLIntegral_sq_lt {g : ℂ → ENNReal} (hg : Measurable g) (ζ : ℂ) {r R : ℝ} (hr : 0 < r) (hrR : r < R) {c : ENNReal} (hc : ENNReal.ofReal (2 * Real.pi) * ∫⁻ (z : ℂ), g z ^ 2 < c * ENNReal.ofReal (Real.log (R / r))) : ∃ ρ ∈ Set.Ioo r R, circleLIntegral g ζ ρ ^ 2 < c

Wolff's lemma. If 2 π times the plane integral of g ^ 2 is smaller than c * log (R / r), then some circle of radius ρ strictly between r and R has circleLIntegral g ζ ρ ^ 2 < c.

Since log (R / r) grows without bound as the annulus is made longer while the plane integral stays fixed, this makes the circle integral arbitrarily small at arbitrarily small radii: a weight of finite square integral cannot have a large circle integral on every circle about ζ.

Small circle integrals at arbitrarily small radii

theorem TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top {g : ℂ → ENNReal} (hg : Measurable g) (hfin : ∫⁻ (z : ℂ), g z ^ 2 ≠ ⊤) (ζ : ℂ) {c : ENNReal} (hc : c ≠ 0) {R : ℝ} (hR : 0 < R) : ∃ ρ ∈ Set.Ioo 0 R, circleLIntegral g ζ ρ < c

Wolff's lemma in the limit: a weight of finite square integral has small circle integrals at arbitrarily small radii. If ∫⁻ z, g z ^ 2 is finite then for every threshold c ≠ 0 and every bound R > 0 there is a radius ρ below R with circleLIntegral g ζ ρ < c.

The threshold that TauCeti.exists_circleLIntegral_sq_lt asks to be beaten is 2 π ∫⁻ z, g z ^ 2 / log (R / r), which for a finite square integral falls to 0 as the annulus Ioo r R is made logarithmically longer; here the outer radius is the prescribed bound R and the inner one R * exp (-L) is pushed towards 0, which is what confines the radius produced to Ioo 0 R. The reduction to a finite threshold is the passage to min c 1, and the square is undone by monotonicity of squaring on ℝ≥0∞.

There is no companion statement for a fixed small radius: see TauCeti.liminf_circleLIntegral_nhdsGT_eq_zero for the sharp form, a lower limit rather than a limit.

theorem TauCeti.liminf_circleLIntegral_nhdsGT_eq_zero {g : ℂ → ENNReal} (hg : Measurable g) (hfin : ∫⁻ (z : ℂ), g z ^ 2 ≠ ⊤) (ζ : ℂ) : Filter.liminf (fun (ρ : ℝ) => circleLIntegral g ζ ρ) (nhdsWithin 0 (Set.Ioi 0)) = 0

The circle integrals of a weight of finite square integral have lower limit 0 at the centre. This is the sharp form of TauCeti.exists_circleLIntegral_lt_of_lintegral_sq_ne_top, which says exactly that every positive threshold is undercut on every interval Ioo 0 R of radii, and those intervals are a basis of 𝓝[>] 0.

The limit itself does not exist in general: the circle integral is only frequently small, as the thin-annulus weight described in the module docstring shows.