Theorems · Theorem · complex analysis

PhragmenLindelof.quadrant_II

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

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace