Theorems · Theorem · complex analysis

MeromorphicAt.meromorphicTrailingCoeffAt_comp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜} {g : 𝕜 → 𝕜},
  MeromorphicAt f (g x) →
    AnalyticAt 𝕜 g x →
      ¬Filter.EventuallyConst g (nhds x) →
        meromorphicTrailingCoeffAt (f ∘ g) x =
          meromorphicTrailingCoeffAt (fun x_1 => g x_1 - g x) x ^ (meromorphicOrderAt f (g x)).untop₀ •
            meromorphicTrailingCoeffAt f (g x)

If g is analytic at x and not locally constant, and f is meromorphic at g x, express the trailing coefficient of f ∘ g at x in terms of g and f.

Defined in

Mathlib.Analysis.Meromorphic.TrailingCoefficient

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace