theorem Real.sub_ne_zero_of_lt {a : ℝ} {b : ℝ} (hab : a < b) : b - a ≠ 0

theorem Complex.DiffContOnCl.id {s : Set ℂ} : DiffContOnCl ℂ id s

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_mapsto_dom {l : ℝ} {u : ℝ} (hul : l < u) {z : ℂ} (hz : z ∈ Complex.HadamardThreeLines.verticalStrip 0 1) : ↑l + z * (↑u - ↑l) ∈ Complex.HadamardThreeLines.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.scale_mapsto_dom_cl {l : ℝ} {u : ℝ} (hul : l < u) {z : ℂ} (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1) : ↑l + z * (↑u - ↑l) ∈ Complex.HadamardThreeLines.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_mem_strip {z : ℂ} {l : ℝ} {u : ℝ} (hul : l < u) (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u) : z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ Complex.HadamardThreeLines.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 (Complex.HadamardThreeLines.verticalStrip l u)) : DiffContOnCl ℂ (Complex.HadamardThreeLines.scale f l u) (Complex.HadamardThreeLines.verticalStrip 0 1)

The function scale f l u is diffContOnCl.

theorem Complex.HadamardThreeLines.scale_bddAbove {E : Type u_1} [NormedAddCommGroup E] {f : ℂ → E} {l : ℝ} {u : ℝ} (hul : l < u) (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip l u)) : BddAbove (norm ∘ Complex.HadamardThreeLines.scale f l u '' Complex.HadamardThreeLines.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 ∈ Complex.re ⁻¹' {l}, ‖f z‖ ≤ a) (z : ℂ) : z ∈ Complex.re ⁻¹' {0} → ‖Complex.HadamardThreeLines.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 ∈ Complex.re ⁻¹' {u}, ‖f z‖ ≤ b) (z : ℂ) : z ∈ Complex.re ⁻¹' {1} → ‖Complex.HadamardThreeLines.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.fun_arg_eq {l : ℝ} {u : ℝ} (hul : l < u) (z : ℂ) : ↑l + (z / (↑u - ↑l) - ↑l / (↑u - ↑l)) * (↑u - ↑l) = z

A technical lemma needed in the proof

theorem Complex.HadamardThreeLines.bound_exp_eq {l : ℝ} {u : ℝ} (hul : l < u) (z : ℂ) : (z / (↑u - ↑l)).re - (↑l / (↑u - ↑l)).re = (z.re - l) / (u - l)

Another technical lemma needed in the proof

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.

theorem Complex.HadamardThreeLines.sSupNormIm_scale_left {E : Type u_1} [NormedAddCommGroup E] (f : ℂ → E) {l : ℝ} {u : ℝ} (hul : l < u) : Complex.HadamardThreeLines.sSupNormIm (Complex.HadamardThreeLines.scale f l u) 0 = Complex.HadamardThreeLines.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) : Complex.HadamardThreeLines.sSupNormIm (Complex.HadamardThreeLines.scale f l u) 1 = Complex.HadamardThreeLines.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 : ℂ) : Complex.HadamardThreeLines.interpStrip (Complex.HadamardThreeLines.scale f l u) ((z - ↑l) / (↑u - ↑l)) = Complex.HadamardThreeLines.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]` to the bounds on a general strip.

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

Hadamard three-line theorem: If f is a bounded function, continuous on the closed strip re ⁻¹' [a,b] and differentiable on open strip re ⁻¹' (a,b), 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-a)/(b-a))) * M(1) ^ ((z.re-a)/(b-a)) holds.

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