Theorems · Theorem · complex analysis

PhragmenLindelof.eqOn_quadrant_I

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

Phragmen-Lindelöf principle in the first quadrant. Let f g : ℂ → E be functions such that * f and g are differentiable in the open first quadrant and are continuous on its closure; * ‖f z‖ and ‖g z‖ are bounded from above by A * exp(B * ‖z‖ ^ c) on the open first quadrant for some A, B, and c < 2; * f is equal to g on the boundary of the first quadrant. Then f is equal to g on the closed first quadrant.

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace