Mittag-Leffler theorem

DefinitionPrincipal part with finitely many coefficients#✓fully proved

For a point \(s \in \mathbb{C}\) and a finitely supported sequence \(c = (c_k)_{k \in \mathbb{N}}\) of complex coefficients, the principal part at \(s\) with coefficients \(c\) is the function \(\mathbb{C} \to \mathbb{C}\) given by \(z \mapsto \sum_k c_k (z - s)^{-(k+1)}\), the sum running over the finitely many \(k\) with \(c_k \neq 0\).

At \(z = s\) every term is taken to be \(0\) (the convention \(0^{-n} = 0\)), so the function has value \(0\) there.

noncomputable def principalPart (s : ℂ) (coeff : ℕ →₀ ℂ) (z : ℂ) : ℂ :=
  ∑ k ∈ coeff.support, coeff k * (z - s) ^ (-(↑k + 1) : ℤ)

Used by 4

Used byMittag-Leffler theorem · Mittag-Leffler theorem, discrete-subspace form · The principal part is analytic away from its pole · The principal part is meromorphic

TheoremThe principal part is analytic away from its pole#✓fully proved

For every \(s \in \mathbb{C}\) and every finitely supported sequence \(c\) of complex coefficients, the principal part at \(s\) with coefficients \(c\) is analytic at every point \(z \neq s\).

theorem principalPart_analyticAt (s : ℂ) (coeff : ℕ →₀ ℂ) (z : ℂ) (hz : z ≠ s) :
    AnalyticAt ℂ (principalPart s coeff) z

Uses 1 · Used by 1

Statement usesPrincipal part with finitely many coefficients

Used byMittag-Leffler theorem, discrete-subspace form

TheoremThe principal part is meromorphic#✓fully proved

For every \(s \in \mathbb{C}\) and every finitely supported sequence \(c\) of complex coefficients, the principal part at \(s\) with coefficients \(c\) is meromorphic at every point of \(\mathbb{C}\).

theorem principalPart_meromorphicAt (s : ℂ) (coeff : ℕ →₀ ℂ) (x : ℂ) :
    MeromorphicAt (principalPart s coeff) x

Uses 1 · Used by 1

Statement usesPrincipal part with finitely many coefficients

Used byMittag-Leffler theorem, discrete-subspace form

TheoremMittag-Leffler theorem, discrete-subspace form#✓fully proved

Let \(S \subseteq \mathbb{C}\) be a closed set that is discrete in the subspace topology, and for each \(s \in S\) let \(c_s\) be a finitely supported sequence of complex coefficients. Then there is a function \(f : \mathbb{C} \to \mathbb{C}\) that is holomorphic on \(\mathbb{C} \setminus S\), meromorphic on all of \(\mathbb{C}\), and such that for every \(s \in S\) the difference between \(f\) and the principal part at \(s\) with coefficients \(c_s\) is analytic at \(s\).

theorem mittag_leffler_of_isDiscrete
    (S : Set ℂ) (hS_closed : IsClosed S)
    (hSdisc : IsDiscrete S)
    (coeff : ↥S → ℕ →₀ ℂ) :
    ∃ f : ℂ → ℂ, DifferentiableOn ℂ f Sᶜ ∧
      (∀ s : ↥S, AnalyticAt ℂ (fun z => f z - principalPart s.val (coeff s) z) s.val) ∧
      MeromorphicOn f Set.univ

Uses 3 · Used by 1

Statement usesPrincipal part with finitely many coefficients

Proof usesThe principal part is analytic away from its pole · The principal part is meromorphic

Used byMittag-Leffler theorem

TheoremMittag-Leffler theorem#✓fully proved

Let \(S \subseteq \mathbb{C}\) be a closed set such that every \(z \in S\) has a radius \(\varepsilon > 0\) for which the punctured disk \(\{w : 0 < |w - z| < \varepsilon\}\) contains no point of \(S\), and for each \(s \in S\) let \(c_s\) be a finitely supported sequence of complex coefficients. Then there is a function \(f : \mathbb{C} \to \mathbb{C}\) that is holomorphic on \(\mathbb{C} \setminus S\), meromorphic on all of \(\mathbb{C}\), and such that for every \(s \in S\) the difference between \(f\) and the principal part at \(s\) with coefficients \(c_s\) is analytic at \(s\).

theorem mittag_leffler
    (S : Set ℂ) (hS_closed : IsClosed S)
    (hS_discrete : ∀ z ∈ S, ∃ ε > 0, (Metric.ball z ε \ {z}) ∩ S = ∅)
    (coeff : ↥S → ℕ →₀ ℂ) :
    ∃ f : ℂ → ℂ, DifferentiableOn ℂ f Sᶜ ∧
      (∀ s : ↥S, AnalyticAt ℂ (fun z => f z - principalPart s.val (coeff s) z) s.val) ∧
      MeromorphicOn f Set.univ

Sources

• Mittag-Leffler theorem, G. Mittag-Leffler, Acta Math. 4 (1884); see Rudin; Lean is closed discrete S with punctured-ball isolation, prescribed finite principal parts via Finsupp, global meromorphic existence holomorphic on Sᶜ.

Uses 2

Statement usesPrincipal part with finitely many coefficients

Proof usesMittag-Leffler theorem, discrete-subspace form

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.