Theorems · Theorem · complex analysis

PhragmenLindelof.horizontal_strip

• 1000+ list: Phragmén–Lindelöf theorem

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b) →
    (∃ 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|))) →
      (∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) → (∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) → a ≤ z.im → 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|.

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace