Theorems · Theorem · complex analysis

PhragmenLindelof.eqOn_right_half_plane_of_superexponential_decay

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

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace