The Borel–Carathéodory inequality

A bound on ‖g‖ on a disk in terms of the supremum of re g on a larger disk.

noncomputable def LZCBorelCaratheodory.boundaryRealSup (g : ℂ → ℂ) (R : ℝ) : ℝ

The supremum of the real part of g on the circle of radius R centered at zero.

Equations

• LZCBorelCaratheodory.boundaryRealSup g R = sSup {x : ℝ | ∃ (ζ : ℂ), ‖ζ‖ = R ∧ x = (g ζ).re}

theorem LZCBorelCaratheodory.real_part_le_boundaryRealSup (g : ℂ → ℂ) (R : ℝ) (h_bdd : BddAbove {x : ℝ | ∃ (ζ : ℂ), ‖ζ‖ = R ∧ x = (g ζ).re}) {ζ : ℂ} (hζ : ‖ζ‖ = R) : (g ζ).re ≤ boundaryRealSup g R

theorem LZCBorelCaratheodory.real_part_le_boundaryRealSup_closedBall (g : ℂ → ℂ) (R : ℝ) (_h_R : 0 < R) (h_holo : ∀ (w : ℂ), ‖w‖ ≤ R → DifferentiableAt ℂ g w) (h_bdd : BddAbove {x : ℝ | ∃ (ζ : ℂ), ‖ζ‖ = R ∧ x = (g ζ).re}) {w : ℂ} (hw : ‖w‖ ≤ R) : (g w).re ≤ boundaryRealSup g R

On the closed ball ‖w‖ ≤ R, the real part of g is bounded by the boundary supremum. This follows from the maximum principle for harmonic functions.

noncomputable def LZCBorelCaratheodory.mobius (a : ℝ) (w : ℂ) : ℂ

Möbius transformation used in the Borel-Carathéodory proof. For a > 0, this maps w ↦ w/(2a - w).

Equations

• LZCBorelCaratheodory.mobius a w = w / (2 * ↑a - w)

theorem LZCBorelCaratheodory.mobius_zero (a : ℝ) : mobius a 0 = 0

theorem LZCBorelCaratheodory.mobius_maps_to_unit_ball (a : ℝ) (ha : 0 < a) (w : ℂ) (hw : w.re < a) : ‖mobius a w‖ < 1

If Re(w) < a, then |mobius a w| < 1.

theorem LZCBorelCaratheodory.mobius_differentiable (a : ℝ) (w : ℂ) (hw : 2 * ↑a - w ≠ 0) : DifferentiableAt ℂ (mobius a) w

The Möbius transformation mobius a is differentiable where 2*a - w ≠ 0.

theorem LZCBorelCaratheodory.mobius_norm_formula (a : ℝ) (ha : 0 < a) (w y : ℂ) (hdenom : 2 * ↑a - w ≠ 0) (heq : w / (2 * ↑a - w) = y) (hy_ne : y ≠ -1) : ‖w‖ = 2 * a * ‖y‖ / ‖1 + y‖

If w/(2a - w) = y, then |w| = 2a|y|/|1+y|. This is a key algebraic step. Requires a > 0 to ensure the formula has the right sign.

theorem LZCBorelCaratheodory.norm_lt_one_of_div_eq (a : ℝ) (ha : 0 < a) (w y : ℂ) (hw : w.re < a) (heq : w / (2 * ↑a - w) = y) : ‖y‖ < 1

Helper lemma: if y = w/(2a - w) and Re(w) < a, then |y| < 1. This avoids duplicating the proof from mobius_maps_to_unit_ball.

theorem LZCBorelCaratheodory.div_one_sub_mono {x y : ℝ} (_hx : 0 ≤ x) (hy : y < 1) (hxy : x ≤ y) : x / (1 - x) ≤ y / (1 - y)

The function t ↦ t/(1-t) is monotonically increasing on [0, 1).

structure LZCBorelCaratheodory.BallToUnitBall (R : ℝ) : Type

A bundled structure for functions that map ball(0, R) into closedBall(0, 1), are holomorphic, and fix the origin. This abstraction prevents excessive unfolding when composing functions like Möbius transformations.

• toFun : ℂ → ℂ

  The underlying function

• maps_to : Set.MapsTo self.toFun (Metric.ball 0 R) (Metric.closedBall 0 1)

  The function maps the ball of radius R into the closed unit ball

• differentiable : DifferentiableOn ℂ self.toFun (Metric.ball 0 R)

  The function is holomorphic on the ball

• maps_zero : self.toFun 0 = 0

  The function fixes 0

@[instance_reducible]

instance LZCBorelCaratheodory.BallToUnitBall.instCoeFunForallComplex (R : ℝ) : CoeFun (BallToUnitBall R) fun (x : BallToUnitBall R) => ℂ → ℂ

Equations

• LZCBorelCaratheodory.BallToUnitBall.instCoeFunForallComplex R = { coe := LZCBorelCaratheodory.BallToUnitBall.toFun }

theorem LZCBorelCaratheodory.BallToUnitBall.schwarz_bound {R : ℝ} (f : BallToUnitBall R) {z : ℂ} (hz : z ∈ Metric.ball 0 R) : ‖f.toFun z‖ ≤ ‖z‖ / R

The Schwarz lemma for bundled ball-to-ball functions

theorem LZCBorelCaratheodory.mobius_inversion_bound (a : ℝ) (ha : 0 < a) (w : ℂ) (hw_re : w.re < a) (y : ℂ) (hdenom : 2 * ↑a - w ≠ 0) (heq : w / (2 * ↑a - w) = y) : ‖w‖ ≤ 2 * a * (‖y‖ / (1 - ‖y‖))

Inversion bound for Möbius transformation: if y = w/(2a - w) and |y| < 1, then |w| ≤ 2a|y|/(1 - |y|).

This lemma is stated without direct reference to mobius to avoid type checking issues.

theorem LZCBorelCaratheodory.borel_caratheodory_point (g : ℂ → ℂ) (R r : ℝ) (h_R : 0 < R) (h_r : r < R) (h_holo : ∀ (z : ℂ), ‖z‖ ≤ R → DifferentiableAt ℂ g z) (h_bdd : BddAbove {x : ℝ | ∃ (ζ : ℂ), ‖ζ‖ = R ∧ x = (g ζ).re}) (z : ℂ) : ‖z‖ ≤ r → ‖g z‖ ≤ 2 * r / (R - r) * (boundaryRealSup g R - (g 0).re) + ‖g 0‖

Borel–Carathéodory Theorem (Point-wise version).

If g : ℂ → ℂ is holomorphic on the closed disk ‖z‖ ≤ R and r < R, then for any z with ‖z‖ ≤ r, we have ‖g z‖ ≤ (2r/(R-r)) * (A - Re(g(0))) + ‖g(0)‖ where A := sup {Re(g(ζ)) : ‖ζ‖ = R}.

Proof strategy:

1. Use maximum modulus principle to show Re(g(w)) ≤ A for all ‖w‖ ≤ R
2. For any ε > 0, construct auxiliary function h_ε mapping ball(0,R) → ball(0,1)
3. Apply Schwarz lemma to h_ε
4. Take ε → 0 to get the final bound