Borel-Carathéodory theorem

This file proves the Borel-Carathéodory theorem: for any function f analytic on the open ball |z| < R such that Re(f z) < M for all |z| < R, we have ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)

Main results

• Complex.borelCaratheodory_zero: The theorem under the assumption f 0 = 0
• Complex.borelCaratheodory: The general version of the theorem

Implementation Notes

The proof applies the Schwarz lemma to the transformed function fun z ↦ f z / (2 * M - f z), which maps the ball |z| < R into the unit disk provided that (f z).re < M for all |z| < R. After obtaining bounds on w, we invert the transformation to recover bounds on f.

Tags

complex analysis, Borel, Carathéodory, analytic function, growth bound

theorem Complex.borelCaratheodory_zero {f : ℂ → ℂ} {M R : ℝ} {z : ℂ} (hM : 0 < M) (hf : DifferentiableOn ℂ f (Metric.ball 0 R)) (hf₁ : Set.MapsTo f (Metric.ball 0 R) {z : ℂ | z.re < M}) (hR : 0 < R) (hz : z ∈ Metric.ball 0 R) (hf₂ : f 0 = 0) : ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)

Borel-Carathéodory theorem for functions vanishing at the origin.

If f is analytic on the open ball ‖z‖ < R, satisfies (f z).re < M for all such z, and f 0 = 0, then ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) for all ‖z‖ < R.

theorem Complex.borelCaratheodory {f : ℂ → ℂ} {M R : ℝ} {z : ℂ} (hM : 0 < M) (hf : DifferentiableOn ℂ f (Metric.ball 0 R)) (hf₁ : Set.MapsTo f (Metric.ball 0 R) {z : ℂ | z.re < M}) (hR : 0 < R) (hz : z ∈ Metric.ball 0 R) : ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)

Borel-Carathéodory theorem.

If f is analytic on the open ball ‖z‖ < R and satisfies (f z).re < M for all such z, then ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) for all ‖z‖ < R.