mathlib documentation

analysis.complex.phragmen_lindelof

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 #

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 #

theorem phragmen_lindelof.is_O_sub_exp_exp {E : Type u_1} [normed_add_comm_group E] {a : } {f g : E} {l : filter } {u : } (hBf : (c : ) (H : c < a) (B : ), f =O[l] λ (z : ), real.exp (B * real.exp (c * |u z|))) (hBg : (c : ) (H : c < a) (B : ), g =O[l] λ (z : ), real.exp (B * real.exp (c * |u z|))) :
(c : ) (H : c < a) (B : ), (f - g) =O[l] λ (z : ), real.exp (B * real.exp (c * |u z|))

An auxiliary lemma that combines two double exponential estimates into a similar estimate on the difference of the functions.

theorem phragmen_lindelof.is_O_sub_exp_rpow {E : Type u_1} [normed_add_comm_group E] {a : } {f g : E} {l : filter } (hBf : (c : ) (H : c < a) (B : ), f =O[filter.comap complex.abs filter.at_top l] λ (z : ), real.exp (B * complex.abs z ^ c)) (hBg : (c : ) (H : c < a) (B : ), g =O[filter.comap complex.abs filter.at_top l] λ (z : ), real.exp (B * complex.abs z ^ c)) :
(c : ) (H : c < a) (B : ), (f - g) =O[filter.comap complex.abs filter.at_top l] λ (z : ), real.exp (B * complex.abs z ^ c)

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 #

theorem phragmen_lindelof.horizontal_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b C : } {f : E} {z : } (hfd : diff_cont_on_cl f (complex.im ⁻¹' set.Ioo a b)) (hB : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.re) filter.at_top filter.principal (complex.im ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.re|))) (hle_a : (z : ), z.im = a f z C) (hle_b : (z : ), z.im = b f z C) (hza : a z.im) (hzb : z.im b) :
f z C

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

theorem phragmen_lindelof.eq_zero_on_horizontal_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b : } {f : E} (hd : diff_cont_on_cl f (complex.im ⁻¹' set.Ioo a b)) (hB : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.re) filter.at_top filter.principal (complex.im ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.re|))) (ha : (z : ), z.im = a f z = 0) (hb : (z : ), z.im = b f z = 0) :

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}.

theorem phragmen_lindelof.eq_on_horizontal_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b : } {f g : E} (hdf : diff_cont_on_cl f (complex.im ⁻¹' set.Ioo a b)) (hBf : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.re) filter.at_top filter.principal (complex.im ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.re|))) (hdg : diff_cont_on_cl g (complex.im ⁻¹' set.Ioo a b)) (hBg : (c : ) (H : c < real.pi / (b - a)) (B : ), g =O[filter.comap (has_abs.abs complex.re) filter.at_top filter.principal (complex.im ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.re|))) (ha : (z : ), z.im = a f z = g z) (hb : (z : ), z.im = b f z = g z) :

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 #

theorem phragmen_lindelof.vertical_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b C : } {f : E} {z : } (hfd : diff_cont_on_cl f (complex.re ⁻¹' set.Ioo a b)) (hB : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.im) filter.at_top filter.principal (complex.re ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.im|))) (hle_a : (z : ), z.re = a f z C) (hle_b : (z : ), z.re = b f z C) (hza : a z.re) (hzb : z.re b) :
f z C

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

theorem phragmen_lindelof.eq_zero_on_vertical_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b : } {f : E} (hd : diff_cont_on_cl f (complex.re ⁻¹' set.Ioo a b)) (hB : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.im) filter.at_top filter.principal (complex.re ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.im|))) (ha : (z : ), z.re = a f z = 0) (hb : (z : ), z.re = b f z = 0) :

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}.

theorem phragmen_lindelof.eq_on_vertical_strip {E : Type u_1} [normed_add_comm_group E] [normed_space E] {a b : } {f g : E} (hdf : diff_cont_on_cl f (complex.re ⁻¹' set.Ioo a b)) (hBf : (c : ) (H : c < real.pi / (b - a)) (B : ), f =O[filter.comap (has_abs.abs complex.im) filter.at_top filter.principal (complex.re ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.im|))) (hdg : diff_cont_on_cl g (complex.re ⁻¹' set.Ioo a b)) (hBg : (c : ) (H : c < real.pi / (b - a)) (B : ), g =O[filter.comap (has_abs.abs complex.im) filter.at_top filter.principal (complex.re ⁻¹' set.Ioo a b)] λ (z : ), real.exp (B * real.exp (c * |z.im|))) (ha : (z : ), z.re = a f z = g z) (hb : (z : ), z.re = b f z = g z) :

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 #

theorem phragmen_lindelof.quadrant_I {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Ioi 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x C) (him : (x : ), 0 x f (x * complex.I) C) (hz_re : 0 z.re) (hz_im : 0 z.im) :
f z C

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.

theorem phragmen_lindelof.eq_zero_on_quadrant_I {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} (hd : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Ioi 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x = 0) (him : (x : ), 0 x f (x * complex.I) = 0) :
set.eq_on f 0 {z : | 0 z.re 0 z.im}

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.

theorem phragmen_lindelof.eq_on_quadrant_I {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} (hdf : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Ioi 0)) (hBf : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hdg : diff_cont_on_cl g (set.Ioi 0 ×ℂ set.Ioi 0)) (hBg : (c : ) (H : c < 2) (B : ), g =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x = g x) (him : (x : ), 0 x f (x * complex.I) = g (x * complex.I)) :
set.eq_on f g {z : | 0 z.re 0 z.im}

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.

theorem phragmen_lindelof.quadrant_II {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Ioi 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x C) (him : (x : ), 0 x f (x * complex.I) C) (hz_re : z.re 0) (hz_im : 0 z.im) :
f z C

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.

theorem phragmen_lindelof.eq_zero_on_quadrant_II {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} (hd : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Ioi 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x = 0) (him : (x : ), 0 x f (x * complex.I) = 0) :
set.eq_on f 0 {z : | z.re 0 0 z.im}

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.

theorem phragmen_lindelof.eq_on_quadrant_II {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} (hdf : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Ioi 0)) (hBf : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hdg : diff_cont_on_cl g (set.Iio 0 ×ℂ set.Ioi 0)) (hBg : (c : ) (H : c < 2) (B : ), g =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Ioi 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x = g x) (him : (x : ), 0 x f (x * complex.I) = g (x * complex.I)) :
set.eq_on f g {z : | z.re 0 0 z.im}

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.

theorem phragmen_lindelof.quadrant_III {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Iio 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x C) (him : (x : ), x 0 f (x * complex.I) C) (hz_re : z.re 0) (hz_im : z.im 0) :
f z C

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.

theorem phragmen_lindelof.eq_zero_on_quadrant_III {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} (hd : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Iio 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x = 0) (him : (x : ), x 0 f (x * complex.I) = 0) :
set.eq_on f 0 {z : | z.re 0 z.im 0}

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.

theorem phragmen_lindelof.eq_on_quadrant_III {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} (hdf : diff_cont_on_cl f (set.Iio 0 ×ℂ set.Iio 0)) (hBf : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hdg : diff_cont_on_cl g (set.Iio 0 ×ℂ set.Iio 0)) (hBg : (c : ) (H : c < 2) (B : ), g =O[filter.comap complex.abs filter.at_top filter.principal (set.Iio 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), x 0 f x = g x) (him : (x : ), x 0 f (x * complex.I) = g (x * complex.I)) :
set.eq_on f g {z : | z.re 0 z.im 0}

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.

theorem phragmen_lindelof.quadrant_IV {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Iio 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x C) (him : (x : ), x 0 f (x * complex.I) C) (hz_re : 0 z.re) (hz_im : z.im 0) :
f z C

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.

theorem phragmen_lindelof.eq_zero_on_quadrant_IV {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E} (hd : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Iio 0)) (hB : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x = 0) (him : (x : ), x 0 f (x * complex.I) = 0) :
set.eq_on f 0 {z : | 0 z.re z.im 0}

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.

theorem phragmen_lindelof.eq_on_quadrant_IV {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} (hdf : diff_cont_on_cl f (set.Ioi 0 ×ℂ set.Iio 0)) (hBf : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hdg : diff_cont_on_cl g (set.Ioi 0 ×ℂ set.Iio 0)) (hBg : (c : ) (H : c < 2) (B : ), g =O[filter.comap complex.abs filter.at_top filter.principal (set.Ioi 0 ×ℂ set.Iio 0)] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : (x : ), 0 x f x = g x) (him : (x : ), x 0 f (x * complex.I) = g (x * complex.I)) :
set.eq_on f g {z : | 0 z.re z.im 0}

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 #

theorem phragmen_lindelof.right_half_plane_of_tendsto_zero_on_real {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f {z : | 0 < z.re}) (hexp : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal {z : | 0 < z.re}] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : filter.tendsto (λ (x : ), f x) filter.at_top (nhds 0)) (him : (x : ), f (x * complex.I) C) (hz : 0 z.re) :
f z C

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 phragmen_lindelof.right_half_plane_of_bounded_on_real for a stronger version.

theorem phragmen_lindelof.right_half_plane_of_bounded_on_real {E : Type u_1} [normed_add_comm_group E] [normed_space E] {C : } {f : E} {z : } (hd : diff_cont_on_cl f {z : | 0 < z.re}) (hexp : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal {z : | 0 < z.re}] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : filter.is_bounded_under has_le.le filter.at_top (λ (x : ), f x)) (him : (x : ), f (x * complex.I) C) (hz : 0 z.re) :
f z C

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 phragmen_lindelof.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.

theorem phragmen_lindelof.eq_on_right_half_plane_of_superexponential_decay {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f g : E} (hfd : diff_cont_on_cl f {z : | 0 < z.re}) (hgd : diff_cont_on_cl g {z : | 0 < z.re}) (hfexp : (c : ) (H : c < 2) (B : ), f =O[filter.comap complex.abs filter.at_top filter.principal {z : | 0 < z.re}] λ (z : ), real.exp (B * complex.abs z ^ c)) (hgexp : (c : ) (H : c < 2) (B : ), g =O[filter.comap complex.abs filter.at_top filter.principal {z : | 0 < z.re}] λ (z : ), real.exp (B * complex.abs z ^ c)) (hre : asymptotics.superpolynomial_decay filter.at_top real.exp (λ (x : ), f x - g x)) (hfim : (C : ), (x : ), f (x * complex.I) C) (hgim : (C : ), (x : ), g (x * complex.I) C) :
set.eq_on f g {z : | 0 z.re}

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.