Radial limits determine a holomorphic function: the F. and M. Riesz uniqueness theorem

A bounded holomorphic function on a disc whose radial limits equal a on a set of angles of positive measure is the constant a. More generally it suffices that the circle averages of log⁺ ‖f‖ stay bounded on circles whose radii accumulate at the radius of the disc, as they do for the functions of bounded characteristic (the Nevanlinna class); for a nonzero such function the set of angles at which its radial limit is 0 is null. Radial limits are taken along r ↦ circleMap c r θ as r increases to the radius R, and the set of angles is an arbitrary subset of ℝ of positive outer measure.

This is not a consequence of the identity principle: the boundary values say nothing about an accumulation point of zeros inside the open disc. In the boundary theory of conformal maps it is the uniqueness input showing that the preimage under a conformal map of a curve ending at a boundary point ends at a single point of the circle, since otherwise the map would tend to that boundary point along almost every radius ending in an arc of the circle.

Main results

• AnalyticOnNhd.le_circleAverage_log_norm — Jensen's inequality from below: the circle average of log ‖f‖ is at least k * log r + log ‖τ‖, where k is the order of f at the centre and τ its trailing coefficient there.
• AnalyticOnNhd.exists_forall_le_circleAverage_log_norm — a uniform lower bound for these averages on circles with radii in [s, R).
• TauCeti.eqOn_zero_ball_of_tendsto_circleMap_of_circleAverage_posLog_le — the sequential form: a function whose circle averages of log⁺ ‖f‖ are bounded on a sequence of circles with radii in [s, R), and whose values on these circles tend to 0 at every angle of a set of positive measure, vanishes on the disc.
• TauCeti.eqOn_zero_ball_of_tendsto_circleMap_of_frequently_circleAverage_posLog_le — a function whose circle averages of log⁺ ‖f‖ are bounded on circles with radii accumulating at R, and whose radial limit is 0 on a set of angles of positive measure, vanishes on the disc.
• TauCeti.eqOn_const_ball_of_tendsto_circleMap_of_frequently_circleAverage_posLog_le — a function whose circle averages of log⁺ ‖f‖ are bounded on circles with radii accumulating at R, and whose radial limit is a on a set of angles of positive measure, is the constant a.
• TauCeti.eqOn_const_ball_of_tendsto_circleMap — a bounded holomorphic function with radial limit a on a set of angles of positive measure is the constant a.

Implementation notes

Suppose f does not vanish identically. Jensen's formula bounds the circle averages of log ‖f‖ from below on circles near the boundary, and log⁺ ‖f‖⁻¹ = log⁺ ‖f‖ - log ‖f‖, so the averages of log⁺ ‖f‖⁻¹ stay bounded along a sequence of radii tending to R. On the angles with radial limit 0, which up to the countably many zeros of f on those circles form a set of positive measure in one period, log⁺ ‖f‖⁻¹ tends to ∞, and Fatou's lemma makes the averages unbounded.

References

• F. Riesz and M. Riesz, Über die Randwerte einer analytischen Funktion, Quatrième Congrès des Mathématiciens Scandinaves, Stockholm (1916), 27–44.
• P. L. Duren, Theory of Hᵖ Spaces, Chapter 2.

theorem AnalyticOnNhd.le_circleAverage_log_norm {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.closedBall c |r|)) (hr : r ≠ 0) : ↑(analyticOrderNatAt f c) * Real.log r + Real.log ‖meromorphicTrailingCoeffAt f c‖ ≤ Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) c r

Jensen's inequality from below. If f is analytic on the closed disc of radius |r| about c, with r ≠ 0, the circle average of log ‖f‖ is at least k * log r + log ‖τ‖, where k is the order of f at c and τ its trailing coefficient there.

This is Jensen's formula MeromorphicOn.circleAverage_log_norm with the contributions of the zeros other than c dropped, each of which is nonnegative.

theorem AnalyticOnNhd.exists_forall_le_circleAverage_log_norm {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hf : AnalyticOnNhd ℂ f (Metric.ball c R)) {s : ℝ} (hs : 0 < s) : ∃ (L : ℝ), ∀ r ∈ Set.Ico s R, L ≤ Real.circleAverage (fun (z : ℂ) => Real.log ‖f z‖) c r

By Jensen's inequality, the circle averages of log ‖f‖ of a function analytic on ball c R are bounded below on the circles about c with radii in [s, R), for any s > 0.

theorem TauCeti.eqOn_zero_ball_of_tendsto_circleMap_of_circleAverage_posLog_le {f : ℂ → ℂ} {c : ℂ} {R : ℝ} {ρ : ℕ → ℝ} {s C : ℝ} {E : Set ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hs : 0 < s) (hρ : ∀ (n : ℕ), ρ n ∈ Set.Ico s R) (hC : ∀ (n : ℕ), Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c (ρ n) ≤ C) (hE : MeasureTheory.volume E ≠ 0) (hlim : ∀ θ ∈ E, Filter.Tendsto (fun (n : ℕ) => f (circleMap c (ρ n) θ)) Filter.atTop (nhds 0)) : Set.EqOn f 0 (Metric.ball c R)

F. and M. Riesz uniqueness theorem, sequential form. Let f be holomorphic on the disc ball c R, and let ρ n ∈ [s, R) be radii, with s > 0, on whose circles about c the averages of log⁺ ‖f‖ are at most C. If f (circleMap c (ρ n) θ) tends to 0 for every angle θ of a set E of positive measure, then f vanishes on the disc.

The radii need not converge. This form applies to boundary values that are only reached along a sequence of circles almost everywhere, as for limits in L² of the circle restrictions.

theorem TauCeti.eqOn_zero_ball_of_tendsto_circleMap_of_frequently_circleAverage_posLog_le {f : ℂ → ℂ} {c : ℂ} {R C : ℝ} {E : Set ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hC : ∃ᶠ (r : ℝ) in nhdsWithin R (Set.Iio R), Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c r ≤ C) (hE : MeasureTheory.volume E ≠ 0) (hlim : ∀ θ ∈ E, Filter.Tendsto (fun (r : ℝ) => f (circleMap c r θ)) (nhdsWithin R (Set.Iio R)) (nhds 0)) : Set.EqOn f 0 (Metric.ball c R)

F. and M. Riesz uniqueness theorem. Let f be holomorphic on the disc ball c R, with circle averages of log⁺ ‖f‖ at most C on circles about c whose radii accumulate at R from below. If the radial limit of f is 0 at every angle of a set E of positive measure, then f vanishes on the disc.

The bound holds for every function of bounded characteristic, in particular for every bounded function (TauCeti.eqOn_const_ball_of_tendsto_circleMap). The radial limit at the angle θ is taken along r ↦ circleMap c r θ as r increases to R.

theorem TauCeti.eqOn_const_ball_of_tendsto_circleMap_of_frequently_circleAverage_posLog_le {f : ℂ → ℂ} {c : ℂ} {R : ℝ} {a : ℂ} {C : ℝ} {E : Set ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hC : ∃ᶠ (r : ℝ) in nhdsWithin R (Set.Iio R), Real.circleAverage (fun (z : ℂ) => ‖f z‖.posLog) c r ≤ C) (hE : MeasureTheory.volume E ≠ 0) (hlim : ∀ θ ∈ E, Filter.Tendsto (fun (r : ℝ) => f (circleMap c r θ)) (nhdsWithin R (Set.Iio R)) (nhds a)) : Set.EqOn f (fun (x : ℂ) => a) (Metric.ball c R)

F. and M. Riesz uniqueness theorem, for an arbitrary limit. Let f be holomorphic on the disc ball c R, with circle averages of log⁺ ‖f‖ at most C on circles about c whose radii accumulate at R from below. If the radial limit of f is a at every angle of a set E of positive measure, then f is the constant a on the disc. The radial limit at the angle θ is taken along r ↦ circleMap c r θ as r increases to R.

theorem TauCeti.eqOn_const_ball_of_tendsto_circleMap {f : ℂ → ℂ} {c : ℂ} {R : ℝ} {a : ℂ} {M : ℝ} {E : Set ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c R)) (hM : ∀ z ∈ Metric.ball c R, ‖f z‖ ≤ M) (hE : MeasureTheory.volume E ≠ 0) (hlim : ∀ θ ∈ E, Filter.Tendsto (fun (r : ℝ) => f (circleMap c r θ)) (nhdsWithin R (Set.Iio R)) (nhds a)) : Set.EqOn f (fun (x : ℂ) => a) (Metric.ball c R)

F. and M. Riesz uniqueness theorem, bounded form. A bounded holomorphic function on the disc ball c R whose radial limit is a at every angle of a set of positive measure is the constant a. The radial limit at the angle θ is taken along r ↦ circleMap c r θ as r increases to R.