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: Iffis a bounded function, continuous onre ⁻¹' [l, u]and differentiable onre ⁻¹' (l, u), then forM(x) := sup ((norm ∘ f) '' (re ⁻¹' {x})), that isM(x)is the supremum of the absolute value offalong the vertical linesre 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 thatlog 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 bComplex.HadamardThreeLines.verticalClosedStrip: The vertical strip defined by :re ⁻¹' Icc a bComplex.HadamardThreeLines.sSupNormIm: The supremum function on vertical lines defined by :sSup {|f(z)| : z.re = x}Complex.HadamardThreeLines.interpStrip: The interpolation between thesSupNormImon the edges of the vertical stripre⁻¹ [0, 1].Complex.HadamardThreeLines.interpStrip: The interpolation between thesSupNormImon the edges of any vertical strip.Complex.HadamardThreeLines.invInterpStrip: Inverse of the interpolation between thesSupNormImon the edges of the vertical stripre⁻¹ [0, 1].Complex.HadamardThreeLines.F: Function defined byftimesinvInterpStrip. 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.
The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Ioo a b.
Instances For
The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Icc a b.
Instances For
The supremum of the norm of f on imaginary lines. (Fixed real part)
This is also known as the function M
Instances For
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
Instances For
A function useful for the proofs steps. We will aim to show that it is bounded by 1.
Instances For
sSup of norm is nonneg applied to the image of f on the vertical line re z = x
sSup of norm translated by ε > 0 is positive applied to the image of f on the
vertical line re z = x
Useful rewrite for the absolute value of invInterpStrip
The function invInterpStrip is diffContOnCl.
If f is bounded on the unit vertical strip, then f is bounded by sSupNormIm there.
Alternative version of norm_le_sSupNormIm with a strict inequality and a positive ε.
When the function f is bounded above on a vertical strip, then so is F.
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.
Instances For
Rewrite for InterpStrip when 0 < sSupNormIm f 0 and 0 < sSupNormIm f 1.
Rewrite for InterpStrip when 0 = sSupNormIm f 0 or 0 = sSupNormIm f 1.
Rewrite for InterpStrip on the open vertical strip.
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.
Instances For
An auxiliary function to prove the general statement of Hadamard's three lines theorem.
Instances For
The transformation on ℂ that is used for scale maps the closed strip re ⁻¹' [l, u]
to the closed strip re ⁻¹' [0, 1].
The norm of the function scale f l u is bounded above on the closed strip re⁻¹' [0, 1].
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.
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.
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]`.
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.
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.
If z is on the closed strip re ⁻¹' [l, u], then (z - l) / (u - l) is on the closed strip
re ⁻¹' [0, 1].
The function scale f l u is diffContOnCl.
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.
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.