Hadamard three-lines Theorem

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

Main result

• norm_le_interp_of_mem_verticalClosedStrip : Hadamard three-line theorem on re ⁻¹' [0,1]: If f is a bounded function, continuous on re ⁻¹' [0,1] and differentiable on re ⁻¹' (0,1), 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 ⁻¹' [0,1] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re 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.

• Complex.HadamardThreeLines.invInterpStrip : Inverse of the interpolation between the sSupNormIm on the edges of the vertical strip.

• 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 ≤ Complex.HadamardThreeLines.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 < ε + Complex.HadamardThreeLines.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) : Complex.abs (Complex.HadamardThreeLines.invInterpStrip f z ε) = (ε + Complex.HadamardThreeLines.sSupNormIm f 0) ^ (z.re - 1) * (ε + Complex.HadamardThreeLines.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 : ℂ) => Complex.HadamardThreeLines.invInterpStrip f z ε) (Complex.HadamardThreeLines.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 ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) : ‖f z‖ ≤ Complex.HadamardThreeLines.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 ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) : ‖f z‖ < ε + Complex.HadamardThreeLines.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 '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) : BddAbove (norm ∘ Complex.HadamardThreeLines.F f ε '' Complex.HadamardThreeLines.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 '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (hz : z ∈ Complex.re ⁻¹' {0, 1}) : ‖Complex.HadamardThreeLines.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 (Complex.HadamardThreeLines.verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : ‖Complex.HadamardThreeLines.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 < Complex.HadamardThreeLines.sSupNormIm f 0) (h1 : 0 < Complex.HadamardThreeLines.sSupNormIm f 1) : Complex.HadamardThreeLines.interpStrip f z = ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.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 : Complex.HadamardThreeLines.sSupNormIm f 0 = 0 ∨ Complex.HadamardThreeLines.sSupNormIm f 1 = 0) : Complex.HadamardThreeLines.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 ∈ Complex.HadamardThreeLines.verticalStrip 0 1) : Complex.HadamardThreeLines.interpStrip f z = ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.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 ℂ (Complex.HadamardThreeLines.interpStrip f) (Complex.HadamardThreeLines.verticalStrip 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 '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)) (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : ‖f z‖ ≤ ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 1)) ^ z‖

theorem Complex.HadamardThreeLines.eventuallyle {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) [NormedSpace ℂ E] (z : ℂ) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)) (hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1) : (fun (x : ℝ) => ‖f z‖) ≤ᶠ[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ‖(↑ε + ↑(Complex.HadamardThreeLines.sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(Complex.HadamardThreeLines.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 (Complex.HadamardThreeLines.verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1) : ‖f z‖ ≤ ‖Complex.HadamardThreeLines.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 ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) : ‖f z‖ ≤ ‖Complex.HadamardThreeLines.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 ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1)) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1)) (ha : ∀ z ∈ Complex.re ⁻¹' {0}, ‖f z‖ ≤ a) (hb : ∀ z ∈ Complex.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.