Theorems · Theorem · complex analysis

Complex.ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {w : ℂ} {f h : ℂ → E},
  Complex.ECanonicalDecomp f h R →
    w ∈ Metric.closedBall 0 R →
      0 < R →
        h w =
          ((∏ᶠ (i : ℂ),
                meromorphicTrailingCoeffAt (Complex.canonicalFactor R i) w ^
                  (MeromorphicOn.divisor f (Metric.ball 0 R)) i) *
              ∏ᶠ (i : ℂ),
                meromorphicTrailingCoeffAt (fun x => x - i) w ^ (-MeromorphicOn.divisor f (Metric.sphere 0 R)) i) •
            meromorphicTrailingCoeffAt f w

Companion lemma to MeromorphicOn.exists_ecanonicalDecomp: In the setting of the extended canonical decomposition, write the function h entirely in terms of f.

Defined in

Mathlib.Analysis.Complex.CanonicalDecomposition

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace