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

theorem PhragmenLindelof.isBigO_sub_exp_exp {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} {u : ℂ → ℝ} (hBf : ∃ c < a, ∃ (B : ℝ), f =O[l] fun (z : ℂ) => Real.exp (B * Real.exp (c * |u z|))) (hBg : ∃ c < a, ∃ (B : ℝ), g =O[l] fun (z : ℂ) => Real.exp (B * Real.exp (c * |u z|))) : ∃ c < a, ∃ (B : ℝ), (f - g) =O[l] fun (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 PhragmenLindelof.isBigO_sub_exp_rpow {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} (hBf : ∃ c < a, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ l] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hBg : ∃ c < a, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ l] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) : ∃ c < a, ∃ (B : ℝ), (f - g) =O[Bornology.cobounded ℂ ⊓ l] fun (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 PhragmenLindelof.horizontal_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ} (hfd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hB : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun (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 PhragmenLindelof.eq_zero_on_horizontal_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E} (hd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hB : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun (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.EqOn 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}.

theorem PhragmenLindelof.eqOn_horizontal_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b)) (hBf : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun (z : ℂ) => Real.exp (B * Real.exp (c * |z.re|))) (hdg : DiffContOnCl ℂ g (Complex.im ⁻¹' Set.Ioo a b)) (hBg : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), g =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓ Filter.principal (Complex.im ⁻¹' Set.Ioo a b)] fun (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.EqOn 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

theorem PhragmenLindelof.vertical_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ} (hfd : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)) (hB : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun (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 PhragmenLindelof.eq_zero_on_vertical_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f : ℂ → E} (hd : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)) (hB : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun (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.EqOn 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}.

theorem PhragmenLindelof.eqOn_vertical_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℝ} {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Complex.re ⁻¹' Set.Ioo a b)) (hBf : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), f =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun (z : ℂ) => Real.exp (B * Real.exp (c * |z.im|))) (hdg : DiffContOnCl ℂ g (Complex.re ⁻¹' Set.Ioo a b)) (hBg : ∃ c < Real.pi / (b - a), ∃ (B : ℝ), g =O[Filter.comap (abs ∘ Complex.im) Filter.atTop ⊓ Filter.principal (Complex.re ⁻¹' Set.Ioo a b)] fun (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.EqOn 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

theorem PhragmenLindelof.quadrant_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun (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 PhragmenLindelof.eq_zero_on_quadrant_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun (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.EqOn 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 PhragmenLindelof.eqOn_quadrant_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Ioi 0)) (hBf : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hdg : DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Ioi 0)) (hBg : ∃ c < 2, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Ioi 0)] fun (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.EqOn 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 PhragmenLindelof.quadrant_II {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ 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 PhragmenLindelof.eq_zero_on_quadrant_II {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ x ≤ 0, f ↑x = 0) (him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = 0) : Set.EqOn 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 PhragmenLindelof.eqOn_quadrant_II {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Ioi 0)) (hBf : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hdg : DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Ioi 0)) (hBg : ∃ c < 2, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Ioi 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ x ≤ 0, f ↑x = g ↑x) (him : ∀ (x : ℝ), 0 ≤ x → f (↑x * Complex.I) = g (↑x * Complex.I)) : Set.EqOn 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 PhragmenLindelof.quadrant_III {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C) (him : ∀ 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 PhragmenLindelof.eq_zero_on_quadrant_III {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hd : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ x ≤ 0, f ↑x = 0) (him : ∀ x ≤ 0, f (↑x * Complex.I) = 0) : Set.EqOn 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 PhragmenLindelof.eqOn_quadrant_III {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Set.Iio 0 ×ℂ Set.Iio 0)) (hBf : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hdg : DiffContOnCl ℂ g (Set.Iio 0 ×ℂ Set.Iio 0)) (hBg : ∃ c < 2, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Iio 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ x ≤ 0, f ↑x = g ↑x) (him : ∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) : Set.EqOn 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 PhragmenLindelof.quadrant_IV {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C) (him : ∀ 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 PhragmenLindelof.eq_zero_on_quadrant_IV {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hd : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0)) (hB : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = 0) (him : ∀ x ≤ 0, f (↑x * Complex.I) = 0) : Set.EqOn 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 PhragmenLindelof.eqOn_quadrant_IV {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hdf : DiffContOnCl ℂ f (Set.Ioi 0 ×ℂ Set.Iio 0)) (hBf : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hdg : DiffContOnCl ℂ g (Set.Ioi 0 ×ℂ Set.Iio 0)) (hBg : ∃ c < 2, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ Filter.principal (Set.Ioi 0 ×ℂ Set.Iio 0)] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : ∀ (x : ℝ), 0 ≤ x → f ↑x = g ↑x) (him : ∀ x ≤ 0, f (↑x * Complex.I) = g (↑x * Complex.I)) : Set.EqOn 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 PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}) (hexp : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 < z.re}] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : Filter.Tendsto (fun (x : ℝ) => f ↑x) Filter.atTop (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 PhragmenLindelof.right_half_plane_of_bounded_on_real for a stronger version.

theorem PhragmenLindelof.right_half_plane_of_bounded_on_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ} (hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}) (hexp : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 < z.re}] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (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 PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real for a weaker version.

theorem PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}) (hexp : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 < z.re}] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun (x : ℝ) => ‖f ↑x‖) (him : ∃ (C : ℝ), ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) : Set.EqOn 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.

theorem PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} (hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}) (hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}) (hfexp : ∃ c < 2, ∃ (B : ℝ), f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 < z.re}] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hgexp : ∃ c < 2, ∃ (B : ℝ), g =O[Bornology.cobounded ℂ ⊓ Filter.principal {z : ℂ | 0 < z.re}] fun (z : ℂ) => Real.exp (B * Complex.abs z ^ c)) (hre : Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun (x : ℝ) => ‖f ↑x - g ↑x‖) (hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) (hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g (↑x * Complex.I)‖ ≤ C) : Set.EqOn 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.