Documentation

Mathlib.Analysis.Complex.PhragmenLindelof

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 #

source
theorem PhragmenLindelof.isBigO_sub_exp_exp {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} {f : ℂ → E} {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.

source
theorem PhragmenLindelof.isBigO_sub_exp_rpow {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} {f : ℂ → E} {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 #

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

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

source
theorem PhragmenLindelof.eqOn_horizontal_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a : ℝ} {b : ℝ} {f : ℂ → E} {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 #

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

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

source
theorem PhragmenLindelof.eqOn_vertical_strip {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a : ℝ} {b : ℝ} {f : ℂ → E} {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 #

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

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

source
theorem PhragmenLindelof.eqOn_quadrant_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {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.

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

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

source
theorem PhragmenLindelof.eqOn_quadrant_II {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {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.

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

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

source
theorem PhragmenLindelof.eqOn_quadrant_III {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {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.

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

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

source
theorem PhragmenLindelof.eqOn_quadrant_IV {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {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 #

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

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

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

source
theorem PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {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.