Theorems · Theorem · complex analysis

MeromorphicAt.meromorphicOrderAt_comp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {g : 𝕜 → 𝕜},
  MeromorphicAt f (g x) →
    AnalyticAt 𝕜 g x →
      ¬Filter.EventuallyConst g (nhds x) →
        meromorphicOrderAt (f ∘ g) x =
          meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 => g x_1 - g x) x)

If g is analytic at x, f is meromorphic at g x, and g is not locally constant near x, the order of f ∘ g is the product of the orders of f and g · - g x.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace