# Phragmen-Lindelöf principle #

In this file we prove several versions of the Phragmen-Lindelöf principle, a version of the maximum modulus principle for an unbounded domain.

## Main statements #

`PhragmenLindelof.horizontal_strip`

: the Phragmen-Lindelö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 Phragmen-Lindelöf principle in a horizontal strip;`PhragmenLindelof.vertical_strip`

: the Phragmen-Lindelö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 Phragmen-Lindelöf principle in a vertical strip;`PhragmenLindelof.quadrant_I`

,`PhragmenLindelof.quadrant_II`

,`PhragmenLindelof.quadrant_III`

,`PhragmenLindelof.quadrant_IV`

: the Phragmen-Lindelö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 Phragmen-Lindelöf principle in the right half-plane;`PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay`

,`PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay`

: extensionality lemmas based on the Phragmen-Lindelöf principle in the right half-plane.

In the case of the right half-plane, we prove a version of the Phragmen-Lindelö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.

### Phragmen-Lindelöf principle in a horizontal strip #

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`

.
Let `f : ℂ → E`

be a function such that

`f`

is differentiable on`U`

and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * exp(c * |re z|))`

on`U`

for some`c < π / (b - a)`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of`U`

.

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|`

.

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`

.
Let `f : ℂ → E`

be a function such that

`f`

is differentiable on`U`

and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * exp(c * |re z|))`

on`U`

for some`c < π / (b - a)`

;`f z = 0`

on the boundary of`U`

.

Then `f`

is equal to zero on the closed strip `{z : ℂ | a ≤ im z ≤ b}`

.

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < im z < b}`

.
Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable on`U`

and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * exp(c * |re z|))`

on`U`

for some`c < π / (b - a)`

;`f z = g z`

on the boundary of`U`

.

Then `f`

is equal to `g`

on the closed strip `{z : ℂ | a ≤ im z ≤ b}`

.

### Phragmen-Lindelöf principle in a vertical strip #

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`

.
Let `f : ℂ → E`

be a function such that

`f`

is differentiable on`U`

and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * exp(c * |im z|))`

on`U`

for some`c < π / (b - a)`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of`U`

.

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|`

.

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`

.
Let `f : ℂ → E`

be a function such that

`f`

is differentiable on`U`

and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * exp(c * |im z|))`

on`U`

for some`c < π / (b - a)`

;`f z = 0`

on the boundary of`U`

.

Then `f`

is equal to zero on the closed strip `{z : ℂ | a ≤ re z ≤ b}`

.

**Phragmen-Lindelöf principle** in a strip `U = {z : ℂ | a < re z < b}`

.
Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable on`U`

and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * exp(c * |im z|))`

on`U`

for some`c < π / (b - a)`

;`f z = g z`

on the boundary of`U`

.

Then `f`

is equal to `g`

on the closed strip `{z : ℂ | a ≤ re z ≤ b}`

.

### Phragmen-Lindelöf principle in coordinate quadrants #

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open first quadrant for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of the first quadrant.

Then `‖f z‖`

is bounded from above by the same constant on the closed first quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open first quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to zero on the boundary of the first quadrant.

Then `f`

is equal to zero on the closed first quadrant.

**Phragmen-Lindelöf principle** in the first quadrant. Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable in the open first quadrant and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * (abs z) ^ c)`

on the open first quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to`g`

on the boundary of the first quadrant.

Then `f`

is equal to `g`

on the closed first quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open second quadrant for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of the second quadrant.

Then `‖f z‖`

is bounded from above by the same constant on the closed second quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open second quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to zero on the boundary of the second quadrant.

Then `f`

is equal to zero on the closed second quadrant.

**Phragmen-Lindelöf principle** in the second quadrant. Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable in the open second quadrant and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * (abs z) ^ c)`

on the open second quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to`g`

on the boundary of the second quadrant.

Then `f`

is equal to `g`

on the closed second quadrant.

**Phragmen-Lindelö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 by`A * exp (B * (abs z) ^ c)`

on the open third quadrant for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of the third quadrant.

Then `‖f z‖`

is bounded from above by the same constant on the closed third quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open third quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to zero on the boundary of the third quadrant.

Then `f`

is equal to zero on the closed third quadrant.

**Phragmen-Lindelöf principle** in the third quadrant. Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable in the open third quadrant and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * (abs z) ^ c)`

on the open third quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to`g`

on the boundary of the third quadrant.

Then `f`

is equal to `g`

on the closed third quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open fourth quadrant for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the boundary of the fourth quadrant.

Then `‖f z‖`

is bounded from above by the same constant on the closed fourth quadrant.

**Phragmen-Lindelö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 by`A * exp(B * (abs z) ^ c)`

on the open fourth quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to zero on the boundary of the fourth quadrant.

Then `f`

is equal to zero on the closed fourth quadrant.

**Phragmen-Lindelöf principle** in the fourth quadrant. Let `f g : ℂ → E`

be functions such that

`f`

and`g`

are differentiable in the open fourth quadrant and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * (abs z) ^ c)`

on the open fourth quadrant for some`A`

,`B`

, and`c < 2`

;`f`

is equal to`g`

on the boundary of the fourth quadrant.

Then `f`

is equal to `g`

on the closed fourth quadrant.

### Phragmen-Lindelöf principle in the right half-plane #

**Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E`

be a function such that

`f`

is differentiable in the open right half-plane and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * (abs z) ^ c)`

on the open right half-plane for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the imaginary axis;`f x → 0`

as`x : ℝ`

tends to infinity.

Then `‖f z‖`

is bounded from above by the same constant on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_bounded_on_real`

for a stronger version.

**Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E`

be a function such that

`f`

is differentiable in the open right half-plane and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * (abs z) ^ c)`

on the open right half-plane for some`c < 2`

;`‖f z‖`

is bounded from above by a constant`C`

on the imaginary axis;`‖f x‖`

is bounded from above by a constant for large real values of`x`

.

Then `‖f z‖`

is bounded from above by `C`

on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real`

for a weaker version.

**Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E`

be a function such that

`f`

is differentiable in the open right half-plane and is continuous on its closure;`‖f z‖`

is bounded from above by`A * exp(B * (abs z) ^ c)`

on the open right half-plane for some`c < 2`

;`‖f z‖`

is bounded from above by a constant on the imaginary axis;`f x`

,`x : ℝ`

, tends to zero superexponentially fast as`x → ∞`

: for any natural`n`

,`exp (n * x) * ‖f x‖`

tends to zero as`x → ∞`

.

Then `f`

is equal to zero on the closed right half-plane.

**Phragmen-Lindelöf principle** in the right half-plane. Let `f g : ℂ → E`

be functions such
that

`f`

and`g`

are differentiable in the open right half-plane and are continuous on its closure;`‖f z‖`

and`‖g z‖`

are bounded from above by`A * exp(B * (abs z) ^ c)`

on the open right half-plane for some`c < 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 as`x → ∞`

: for any natural`n`

,`exp (n * x) * ‖f x - g x‖`

tends to zero as`x → ∞`

.

Then `f`

is equal to `g`

on the closed right half-plane.