Theorems · Theorem · complex analysis

PhragmenLindelof.eq_zero_on_right_half_plane_of_superexponential_decay

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E},
  DiffContOnCl ℂ f {z | 0 < z.re} →
    (∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (Asymptotics.SuperpolynomialDecay Filter.atTop Real.exp fun x => ‖f ↑x‖) →
        (∃ 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 * ‖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.

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

1 results in Mathlib

Foundations

Depth 296 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace