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 #

phragmen_lindelof.horizontal_strip: the Phragmen-Lindelöf principle in a horizontal strip {z : ℂ | a < complex.im z < b};
phragmen_lindelof.eq_zero_on_horizontal_strip, phragmen_lindelof.eq_on_horizontal_strip: extensionality lemmas based on the Phragmen-Lindelöf principle in a horizontal strip;
phragmen_lindelof.vertical_strip: the Phragmen-Lindelöf principle in a vertical strip {z : ℂ | a < complex.re z < b};
phragmen_lindelof.eq_zero_on_vertical_strip, phragmen_lindelof.eq_on_vertical_strip: extensionality lemmas based on the Phragmen-Lindelöf principle in a vertical strip;
phragmen_lindelof.quadrant_I, phragmen_lindelof.quadrant_II, phragmen_lindelof.quadrant_III, phragmen_lindelof.quadrant_IV: the Phragmen-Lindelöf principle in the coordinate quadrants;
phragmen_lindelof.right_half_plane_of_tendsto_zero_on_real, phragmen_lindelof.right_half_plane_of_bounded_on_real: two versions of the Phragmen-Lindelöf principle in the right half-plane;
phragmen_lindelof.eq_zero_on_right_half_plane_of_superexponential_decay, phragmen_lindelof.eq_on_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 #

source

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.

source

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 #

source

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

source

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) :

set.eq_on f 0 (complex.im ⁻¹' set.Icc a b)

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

source

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) :

set.eq_on f g (complex.im ⁻¹' set.Icc a 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 #

source

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

source

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) :

set.eq_on f 0 (complex.re ⁻¹' set.Icc a b)

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

source

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) :

set.eq_on f g (complex.re ⁻¹' set.Icc a 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 #

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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 #

source

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.

source

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.

source

theorem phragmen_lindelof.eq_zero_on_right_half_plane_of_superexponential_decay {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℂ → E} (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 : asymptotics.superpolynomial_decay filter.at_top real.exp (λ (x : ℝ), ∥f ↑x∥)) (him : ∃ (C : ℝ), ∀ (x : ℝ), ∥f (↑x * complex.I)∥ ≤ C) :

set.eq_on f 0 {z : ℂ | 0 ≤ z.re}

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.

source

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.