Hadamard three-lines Theorem

In this file we present a proof of Hadamard's three-lines Theorem.

Main result

• norm_le_interp_of_mem_verticalClosedStrip : Hadamard three-line theorem: If f is a bounded function, continuous on re ⁻¹' [l, u] and differentiable on re ⁻¹' (l, u), then for M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x})), that is M(x) is the supremum of the absolute value of f along the vertical lines re z = x, we have that ∀ z ∈ re ⁻¹' [l, u] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l)) holds. This can be seen to be equivalent to the statement that log M(re z) is a convex function on [0, 1].

• norm_le_interp_of_mem_verticalClosedStrip' : Variant of the above lemma in simpler terms. In particular, it makes no mention of the helper functions defined in this file.

Main definitions

• Complex.HadamardThreeLines.verticalStrip : The vertical strip defined by : re ⁻¹' Ioo a b

• Complex.HadamardThreeLines.verticalClosedStrip : The vertical strip defined by : re ⁻¹' Icc a b

• Complex.HadamardThreeLines.sSupNormIm : The supremum function on vertical lines defined by : sSup {|f(z)| : z.re = x}

• Complex.HadamardThreeLines.interpStrip : The interpolation between the sSupNormIm on the edges of the vertical strip re⁻¹ [0, 1].

• Complex.HadamardThreeLines.interpStrip : The interpolation between the sSupNormIm on the edges of any vertical strip.

• Complex.HadamardThreeLines.invInterpStrip : Inverse of the interpolation between the sSupNormIm on the edges of the vertical strip re⁻¹ [0, 1].

• Complex.HadamardThreeLines.F : Function defined by f times invInterpStrip. Convenient form for proofs.

Note

The proof follows from Phragmén-Lindelöf when both frontiers are not everywhere zero. We then use a limit argument to cover the case when either of the sides are 0.

def Complex.HadamardThreeLines.verticalStrip (a b : ℝ) : Set ℂ

The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Ioo a b.

Equations

• Complex.HadamardThreeLines.verticalStrip a b = Complex.re ⁻¹' Set.Ioo a b

def Complex.HadamardThreeLines.verticalClosedStrip (a b : ℝ) : Set ℂ

The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Icc a b.

Equations

• Complex.HadamardThreeLines.verticalClosedStrip a b = Complex.re ⁻¹' Set.Icc a b

noncomputable def Complex.HadamardThreeLines.sSupNormIm {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (x : ℝ) : ℝ

The supremum of the norm of f on imaginary lines. (Fixed real part) This is also known as the function M

Equations

• Complex.HadamardThreeLines.sSupNormIm f x = sSup (norm ∘ f '' (Complex.re ⁻¹' {x}))

noncomputable def Complex.HadamardThreeLines.invInterpStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (ε : ℝ) : ℂ

The inverse of the interpolation of sSupNormIm on the two boundaries. In other words, this is the inverse of the right side of the target inequality: |f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|.

Shifting this by a positive epsilon allows us to prove the case when either of the boundaries is zero.

Equations

• Complex.HadamardThreeLines.invInterpStrip f z ε = (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (z - 1) * (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ (-z)

noncomputable def Complex.HadamardThreeLines.F {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) [NormedSpace ℂ E] (ε : ℝ) (z : ℂ) : E

A function useful for the proofs steps. We will aim to show that it is bounded by 1.

Equations

• Complex.HadamardThreeLines.F f ε z = Complex.HadamardThreeLines.invInterpStrip f z ε • f z

theorem Complex.HadamardThreeLines.sSupNormIm_nonneg {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (x : ℝ) : 0 ≤ sSupNormIm f x

sSup of norm is nonneg applied to the image of f on the vertical line re z = x

theorem Complex.HadamardThreeLines.sSupNormIm_eps_pos {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {ε : ℝ} (hε : ε > 0) (x : ℝ) : 0 < ε + sSupNormIm f x

sSup of norm translated by ε > 0 is positive applied to the image of f on the vertical line re z = x

theorem Complex.HadamardThreeLines.abs_invInterpStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) {ε : ℝ} (hε : ε > 0) : abs (invInterpStrip f z ε) = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Useful rewrite for the absolute value of invInterpStrip

theorem Complex.HadamardThreeLines.diffContOnCl_invInterpStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {ε : ℝ} (hε : ε > 0) : DiffContOnCl ℂ (fun (z : ℂ) => invInterpStrip f z ε) (verticalStrip 0 1)

The function invInterpStrip is diffContOnCl.

theorem Complex.HadamardThreeLines.norm_le_sSupNormIm {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (hD : z ∈ verticalClosedStrip 0 1) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) : ‖f z‖ ≤ sSupNormIm f z.re

If f is bounded on the unit vertical strip, then f is bounded by sSupNormIm there.

theorem Complex.HadamardThreeLines.norm_lt_sSupNormIm_eps {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (z : ℂ) (hD : z ∈ verticalClosedStrip 0 1) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) : ‖f z‖ < ε + sSupNormIm f z.re

Alternative version of norm_le_sSupNormIm with a strict inequality and a positive ε.

theorem Complex.HadamardThreeLines.F_BddAbove {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) : BddAbove (norm ∘ F f ε '' verticalClosedStrip 0 1)

When the function f is bounded above on a vertical strip, then so is F.

theorem Complex.HadamardThreeLines.F_edge_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (ε : ℝ) (hε : ε > 0) (z : ℂ) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (hz : z ∈ re ⁻¹' {0, 1}) : ‖F f ε z‖ ≤ 1

Proof that F is bounded by one one the edges.

theorem Complex.HadamardThreeLines.norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (ε : ℝ) (hε : 0 < ε) (z : ℂ) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (hz : z ∈ verticalClosedStrip 0 1) : ‖F f ε z‖ ≤ 1

noncomputable def Complex.HadamardThreeLines.interpStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) : ℂ

The interpolation of sSupNormIm on the two boundaries. In other words, this is the right side of the target inequality: |f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|.

Note that if sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0 then the power is not continuous since 0 ^ 0 = 1. Hence the use of ite.

Equations

• One or more equations did not get rendered due to their size.

theorem Complex.HadamardThreeLines.interpStrip_eq_of_pos {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (h0 : 0 < sSupNormIm f 0) (h1 : 0 < sSupNormIm f 1) : interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Rewrite for InterpStrip when 0 < sSupNormIm f 0 and 0 < sSupNormIm f 1.

theorem Complex.HadamardThreeLines.interpStrip_eq_of_zero {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0) : interpStrip f z = 0

Rewrite for InterpStrip when 0 = sSupNormIm f 0 or 0 = sSupNormIm f 1.

theorem Complex.HadamardThreeLines.interpStrip_eq_of_mem_verticalStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (z : ℂ) (hz : z ∈ verticalStrip 0 1) : interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Rewrite for InterpStrip on the open vertical strip.

theorem Complex.HadamardThreeLines.diffContOnCl_interpStrip {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) : DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

noncomputable def Complex.HadamardThreeLines.interpStrip' {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) (l u : ℝ) (z : ℂ) : ℂ

The correct generalization of interpStrip to produce bounds in the general case.

Equations

• One or more equations did not get rendered due to their size.

def Complex.HadamardThreeLines.scale {E : Type u_1} (f : ℂ → E) (l u : ℝ) : ℂ → E

An auxiliary function to prove the general statement of Hadamard's three lines theorem.

Equations

• Complex.HadamardThreeLines.scale f l u z = f (↑l + z • (↑u - ↑l))

theorem Complex.HadamardThreeLines.scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip {l u : ℝ} (hul : l < u) {z : ℂ} (hz : z ∈ verticalClosedStrip 0 1) : ↑l + z * (↑u - ↑l) ∈ verticalClosedStrip l u

The transformation on ℂ that is used for scale maps the closed strip re ⁻¹' [l, u] to the closed strip re ⁻¹' [0, 1].

theorem Complex.HadamardThreeLines.scale_bddAbove {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {l u : ℝ} (hul : l < u) (hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)) : BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

The norm of the function scale f l u is bounded above on the closed strip re⁻¹' [0, 1].

theorem Complex.HadamardThreeLines.scale_bound_left {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {l u a : ℝ} (ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a) (z : ℂ) : z ∈ re ⁻¹' {0} → ‖scale f l u z‖ ≤ a

A bound to the norm of f on the line z.re = l induces a bound to the norm of scale f l u z on the line z.re = 0.

theorem Complex.HadamardThreeLines.scale_bound_right {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {l u b : ℝ} (hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b) (z : ℂ) : z ∈ re ⁻¹' {1} → ‖scale f l u z‖ ≤ b

A bound to the norm of f on the line z.re = u induces a bound to the norm of scale f l u z on the line z.re = 1.

theorem Complex.HadamardThreeLines.sSupNormIm_scale_left {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ} (hul : l < u) : sSupNormIm (scale f l u) 0 = sSupNormIm f l

The supremum of the norm of scale f l u on the line z.re = 0 is the same as the supremum of f on the line z.re = l.

theorem Complex.HadamardThreeLines.sSupNormIm_scale_right {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ} (hul : l < u) : sSupNormIm (scale f l u) 1 = sSupNormIm f u

The supremum of the norm of scale f l u on the line z.re = 1 is the same as the supremum of f on the line z.re = u.

theorem Complex.HadamardThreeLines.interpStrip_scale {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {l u : ℝ} (hul : l < u) (z : ℂ) : interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z

A technical lemma relating the bounds given by the three lines lemma on a general strip to the bounds for its scaled version on the strip ``re ⁻¹' [0, 1]`.

theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip_eps {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) [NormedSpace ℂ E] (ε : ℝ) (hε : ε > 0) (z : ℂ) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hz : z ∈ verticalClosedStrip 0 1) : ‖f z‖ ≤ ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

theorem Complex.HadamardThreeLines.eventuallyle {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) [NormedSpace ℂ E] (z : ℂ) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hz : z ∈ verticalStrip 0 1) : (fun (x : ℝ) => ‖f z‖) ≤ᶠ[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zero {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) [NormedSpace ℂ E] (z : ℂ) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (hz : z ∈ verticalStrip 0 1) : ‖f z‖ ≤ ‖interpStrip f z‖

theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) {z : ℂ} (hz : z ∈ verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) : ‖f z‖ ≤ ‖interpStrip f z‖

Hadamard three-line theorem on re ⁻¹' [0, 1]: If f is a bounded function, continuous on the closed strip re ⁻¹' [0, 1] and differentiable on open strip re ⁻¹' (0, 1), then for M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x})) we have that for all z in the closed strip re ⁻¹' [0, 1] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re holds.

theorem Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) {z : ℂ} {a b : ℝ} (hz : z ∈ verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)) (ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a) (hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b) : ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re

Hadamard three-line theorem on re ⁻¹' [0, 1] (Variant in simpler terms): Let f be a bounded function, continuous on the closed strip re ⁻¹' [0, 1] and differentiable on open strip re ⁻¹' (0, 1). If, for all z.re = 0, ‖f z‖ ≤ a for some a ∈ ℝ and, similarly, for all z.re = 1, ‖f z‖ ≤ b for some b ∈ ℝ then for all z in the closed strip re ⁻¹' [0, 1] the inequality ‖f(z)‖ ≤ a ^ (1 - z.re) * b ^ z.re holds.

theorem Complex.HadamardThreeLines.scale_id_mem_verticalStrip_of_mem_verticalStrip {l u : ℝ} (hul : l < u) {z : ℂ} (hz : z ∈ verticalStrip 0 1) : ↑l + z * (↑u - ↑l) ∈ verticalStrip l u

The transformation on ℂ that is used for scale maps the strip re ⁻¹' (l, u) to the strip re ⁻¹' (0, 1).

theorem Complex.HadamardThreeLines.mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip {z : ℂ} {l u : ℝ} (hul : l < u) (hz : z ∈ verticalClosedStrip l u) : z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ verticalClosedStrip 0 1

If z is on the closed strip re ⁻¹' [l, u], then (z - l) / (u - l) is on the closed strip re ⁻¹' [0, 1].

theorem Complex.HadamardThreeLines.scale_diffContOnCl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {l u : ℝ} (hul : l < u) (hd : DiffContOnCl ℂ f (verticalStrip l u)) : DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1)

The function scale f l u is diffContOnCl.

theorem Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {l u : ℝ} (hul : l < u) {f : ℂ → E} {z : ℂ} (hz : z ∈ verticalClosedStrip l u) (hd : DiffContOnCl ℂ f (verticalStrip l u)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)) : ‖f z‖ ≤ ‖interpStrip' f l u z‖

Hadamard three-line theorem: If f is a bounded function, continuous on the closed strip re ⁻¹' [l, u] and differentiable on open strip re ⁻¹' (l, u), then for M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x})) we have that for all z in the closed strip re ⁻¹' [a,b] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l)) holds.

theorem Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {z : ℂ} {a b l u : ℝ} (hul : l < u) (hz : z ∈ verticalClosedStrip l u) (hd : DiffContOnCl ℂ f (verticalStrip l u)) (hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)) (ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a) (hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b) : ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))

Hadamard three-line theorem (Variant in simpler terms): Let f be a bounded function, continuous on the closed strip re ⁻¹' [l, u] and differentiable on open strip re ⁻¹' (l, u). If, for all z.re = l, ‖f z‖ ≤ a for some a ∈ ℝ and, similarly, for all z.re = u, ‖f z‖ ≤ b for some b ∈ ℝ then for all z in the closed strip re ⁻¹' [l, u] the inequality ‖f(z)‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l)) holds.