Theorems · Theorem · complex analysis

PhragmenLindelof.right_half_plane_of_bounded_on_real

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  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)) →
      (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun x => ‖f ↑x‖) →
        (∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → 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 * ‖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.

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace