Theorems · Theorem · complex analysis

PhragmenLindelof.isBigO_sub_exp_rpow

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {a : ℝ} {f g : ℂ → E} {l : Filter ℂ},
  (∃ c < a, ∃ B, f =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)) →
    (∃ c < a, ∃ B, g =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)) →
      ∃ c < a, ∃ B, (f - g) =O[Bornology.cobounded ℂ ⊓ l] fun z => Real.exp (B * ‖z‖ ^ c)

An auxiliary lemma that combines two “exponential of a power” estimates into a similar estimate on the difference of the functions.

Defined in

Mathlib.Analysis.Complex.PhragmenLindelof

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup