PhragmenLindelöf principle #
In this file we prove several versions of the PhragmenLindelöf principle, a version of the maximum modulus principle for an unbounded domain.
Main statements #

PhragmenLindelof.horizontal_strip
: the PhragmenLindelöf principle in a horizontal strip{z : ℂ  a < complex.im z < b}
; 
PhragmenLindelof.eq_zero_on_horizontal_strip
,PhragmenLindelof.eqOn_horizontal_strip
: extensionality lemmas based on the PhragmenLindelöf principle in a horizontal strip; 
PhragmenLindelof.vertical_strip
: the PhragmenLindelöf principle in a vertical strip{z : ℂ  a < complex.re z < b}
; 
PhragmenLindelof.eq_zero_on_vertical_strip
,PhragmenLindelof.eqOn_vertical_strip
: extensionality lemmas based on the PhragmenLindelöf principle in a vertical strip; 
PhragmenLindelof.quadrant_I
,PhragmenLindelof.quadrant_II
,PhragmenLindelof.quadrant_III
,PhragmenLindelof.quadrant_IV
: the PhragmenLindelöf principle in the coordinate quadrants; 
PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real
,PhragmenLindelof.right_half_plane_of_bounded_on_real
: two versions of the PhragmenLindelöf principle in the right halfplane; 
PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay
,PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay
: extensionality lemmas based on the PhragmenLindelöf principle in the right halfplane.
In the case of the right halfplane, we prove a version of the PhragmenLindelöf principle that is useful for Ilyashenko's proof of the individual finiteness theorem (a polynomial vector field on the real plane has only finitely many limit cycles).
Auxiliary lemmas #
An auxiliary lemma that combines two double exponential estimates into a similar estimate on the difference of the functions.
An auxiliary lemma that combines two “exponential of a power” estimates into a similar estimate on the difference of the functions.
PhragmenLindelöf principle in a horizontal strip #
PhragmenLindelöf principle in a strip U = {z : ℂ  a < im z < b}
.
Let f : ℂ → E
be a function such that
f
is differentiable onU
and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * exp(c * re z))
onU
for somec < π / (b  a)
;‖f z‖
is bounded from above by a constantC
on the boundary ofU
.
Then ‖f z‖
is bounded by the same constant on the closed strip
{z : ℂ  a ≤ im z ≤ b}
. Moreover, it suffices to verify the second assumption
only for sufficiently large values of re z
.
PhragmenLindelöf principle in a strip U = {z : ℂ  a < im z < b}
.
Let f : ℂ → E
be a function such that
f
is differentiable onU
and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * exp(c * re z))
onU
for somec < π / (b  a)
;f z = 0
on the boundary ofU
.
Then f
is equal to zero on the closed strip {z : ℂ  a ≤ im z ≤ b}
.
PhragmenLindelöf principle in a strip U = {z : ℂ  a < im z < b}
.
Let f g : ℂ → E
be functions such that
f
andg
are differentiable onU
and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * exp(c * re z))
onU
for somec < π / (b  a)
;f z = g z
on the boundary ofU
.
Then f
is equal to g
on the closed strip {z : ℂ  a ≤ im z ≤ b}
.
PhragmenLindelöf principle in a vertical strip #
PhragmenLindelöf principle in a strip U = {z : ℂ  a < re z < b}
.
Let f : ℂ → E
be a function such that
f
is differentiable onU
and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * exp(c * im z))
onU
for somec < π / (b  a)
;‖f z‖
is bounded from above by a constantC
on the boundary ofU
.
Then ‖f z‖
is bounded by the same constant on the closed strip
{z : ℂ  a ≤ re z ≤ b}
. Moreover, it suffices to verify the second assumption
only for sufficiently large values of im z
.
PhragmenLindelöf principle in a strip U = {z : ℂ  a < re z < b}
.
Let f : ℂ → E
be a function such that
f
is differentiable onU
and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * exp(c * im z))
onU
for somec < π / (b  a)
;f z = 0
on the boundary ofU
.
Then f
is equal to zero on the closed strip {z : ℂ  a ≤ re z ≤ b}
.
PhragmenLindelöf principle in a strip U = {z : ℂ  a < re z < b}
.
Let f g : ℂ → E
be functions such that
f
andg
are differentiable onU
and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * exp(c * im z))
onU
for somec < π / (b  a)
;f z = g z
on the boundary ofU
.
Then f
is equal to g
on the closed strip {z : ℂ  a ≤ re z ≤ b}
.
PhragmenLindelöf principle in coordinate quadrants #
PhragmenLindelöf principle in the first quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open first quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open first quadrant for somec < 2
;‖f z‖
is bounded from above by a constantC
on the boundary of the first quadrant.
Then ‖f z‖
is bounded from above by the same constant on the closed first quadrant.
PhragmenLindelöf principle in the first quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open first quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open first quadrant for someA
,B
, andc < 2
;f
is equal to zero on the boundary of the first quadrant.
Then f
is equal to zero on the closed first quadrant.
PhragmenLindelöf principle in the first quadrant. Let f g : ℂ → E
be functions such that
f
andg
are differentiable in the open first quadrant and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * (abs z) ^ c)
on the open first quadrant for someA
,B
, andc < 2
;f
is equal tog
on the boundary of the first quadrant.
Then f
is equal to g
on the closed first quadrant.
PhragmenLindelöf principle in the second quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open second quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open second quadrant for somec < 2
;‖f z‖
is bounded from above by a constantC
on the boundary of the second quadrant.
Then ‖f z‖
is bounded from above by the same constant on the closed second quadrant.
PhragmenLindelöf principle in the second quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open second quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open second quadrant for someA
,B
, andc < 2
;f
is equal to zero on the boundary of the second quadrant.
Then f
is equal to zero on the closed second quadrant.
PhragmenLindelöf principle in the second quadrant. Let f g : ℂ → E
be functions such that
f
andg
are differentiable in the open second quadrant and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * (abs z) ^ c)
on the open second quadrant for someA
,B
, andc < 2
;f
is equal tog
on the boundary of the second quadrant.
Then f
is equal to g
on the closed second quadrant.
PhragmenLindelöf principle in the third quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open third quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp (B * (abs z) ^ c)
on the open third quadrant for somec < 2
;‖f z‖
is bounded from above by a constantC
on the boundary of the third quadrant.
Then ‖f z‖
is bounded from above by the same constant on the closed third quadrant.
PhragmenLindelöf principle in the third quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open third quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open third quadrant for someA
,B
, andc < 2
;f
is equal to zero on the boundary of the third quadrant.
Then f
is equal to zero on the closed third quadrant.
PhragmenLindelöf principle in the third quadrant. Let f g : ℂ → E
be functions such that
f
andg
are differentiable in the open third quadrant and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * (abs z) ^ c)
on the open third quadrant for someA
,B
, andc < 2
;f
is equal tog
on the boundary of the third quadrant.
Then f
is equal to g
on the closed third quadrant.
PhragmenLindelöf principle in the fourth quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open fourth quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open fourth quadrant for somec < 2
;‖f z‖
is bounded from above by a constantC
on the boundary of the fourth quadrant.
Then ‖f z‖
is bounded from above by the same constant on the closed fourth quadrant.
PhragmenLindelöf principle in the fourth quadrant. Let f : ℂ → E
be a function such that
f
is differentiable in the open fourth quadrant and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open fourth quadrant for someA
,B
, andc < 2
;f
is equal to zero on the boundary of the fourth quadrant.
Then f
is equal to zero on the closed fourth quadrant.
PhragmenLindelöf principle in the fourth quadrant. Let f g : ℂ → E
be functions such that
f
andg
are differentiable in the open fourth quadrant and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * (abs z) ^ c)
on the open fourth quadrant for someA
,B
, andc < 2
;f
is equal tog
on the boundary of the fourth quadrant.
Then f
is equal to g
on the closed fourth quadrant.
PhragmenLindelöf principle in the right halfplane #
PhragmenLindelöf principle in the right halfplane. Let f : ℂ → E
be a function such that
f
is differentiable in the open right halfplane and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open right halfplane for somec < 2
;‖f z‖
is bounded from above by a constantC
on the imaginary axis;f x → 0
asx : ℝ
tends to infinity.
Then ‖f z‖
is bounded from above by the same constant on the closed right halfplane.
See also PhragmenLindelof.right_half_plane_of_bounded_on_real
for a stronger version.
PhragmenLindelöf principle in the right halfplane. Let f : ℂ → E
be a function such that
f
is differentiable in the open right halfplane and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open right halfplane for somec < 2
;‖f z‖
is bounded from above by a constantC
on the imaginary axis;‖f x‖
is bounded from above by a constant for large real values ofx
.
Then ‖f z‖
is bounded from above by C
on the closed right halfplane.
See also PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real
for a weaker version.
PhragmenLindelöf principle in the right halfplane. Let f : ℂ → E
be a function such that
f
is differentiable in the open right halfplane and is continuous on its closure;‖f z‖
is bounded from above byA * exp(B * (abs z) ^ c)
on the open right halfplane for somec < 2
;‖f z‖
is bounded from above by a constant on the imaginary axis;f x
,x : ℝ
, tends to zero superexponentially fast asx → ∞
: for any naturaln
,exp (n * x) * ‖f x‖
tends to zero asx → ∞
.
Then f
is equal to zero on the closed right halfplane.
PhragmenLindelöf principle in the right halfplane. Let f g : ℂ → E
be functions such
that
f
andg
are differentiable in the open right halfplane and are continuous on its closure;‖f z‖
and‖g z‖
are bounded from above byA * exp(B * (abs z) ^ c)
on the open right halfplane for somec < 2
;‖f z‖
and‖g z‖
are bounded from above by constants on the imaginary axis;f x  g x
,x : ℝ
, tends to zero superexponentially fast asx → ∞
: for any naturaln
,exp (n * x) * ‖f x  g x‖
tends to zero asx → ∞
.
Then f
is equal to g
on the closed right halfplane.