Convergent Laurent series on concentric annuli

Let E be a complex normed space. This file defines convergent Laurent series on open concentric annuli Metric.eball c R \ Metric.closedBall c r (0 ≤ r, ENNReal.ofReal r < R, including punctured open disks when r = 0, exteriors of closed disks when R = ⊤, and the whole punctured plane ℂ \ {c} when r = 0 and R = ⊤) and establishes their analytic properties.

Any integer-indexed Laurent series that converges pointwise on an open annulus automatically has summable norm bounds ∑_{n ∈ ℤ} ‖a n‖ * ρ ^ n < ∞ on every interior circle ρ ∈ (r, R) and converges uniformly on every closed concentric subannulus. For complete E, it splits on the open annulus as f = laurentPosPart a c + laurentNegPart a c, where laurentPosPart a c converges as a formal power series on the entire outer disk Metric.eball c R and laurentNegPart a c is complex-analytic on the entire exterior (Metric.closedBall c r)ᶜ and vanishes at infinity. When all negative-degree coefficients vanish on a punctured disk (r = 0), updating f at c with a 0 extends f to a power-series-analytic function on all of Metric.eball c R.

Circle-integral coefficient extraction, uniqueness, Laurent's theorem for holomorphic functions on annuli, removable-singularity characterization, and term-by-term differentiation are developed in TauCeti.Analysis.Complex.Laurent.Expansion.

Main definitions

• TauCeti.HasLaurentSeriesOnAnnulus f a c r R: 0 ≤ r, ENNReal.ofReal r < R, and the integer-indexed series ∑_{n ∈ ℤ} (w - c) ^ n • a n has sum f w at every point w of the open annulus Metric.eball c R \ Metric.closedBall c r.
• TauCeti.laurentPosPowerSeries a: the formal multilinear power series with n-th coefficient a n (n : ℕ), which equals cauchyPowerSeries f c R for a = circleLaurentCoeff f c R.
• TauCeti.laurentPosPart a c: the nonnegative sum w ↦ ∑' n : ℕ, (w - c) ^ n • a n.
• TauCeti.laurentNegPart a c: the principal sum w ↦ ∑' n : ℕ, (w - c) ^ (-((n : ℤ) + 1)) • a (-((n : ℤ) + 1)).

Main results

• HasFPowerSeriesOnBall.hasLaurentSeriesOnAnnulus: views a formal power series on Metric.eball c R as a Laurent series on Metric.eball c R \ {c} with vanishing negative coefficients.
• TauCeti.HasLaurentSeriesOnAnnulus.summable_norm_mul_zpow and TauCeti.HasLaurentSeriesOnAnnulus.tendstoUniformlyOn_closedAnnulus: automatic absolute summability on interior circles and uniform convergence on closed concentric subannuli.
• TauCeti.HasLaurentSeriesOnAnnulus.hasFPowerSeriesOnBall_laurentPosPart, TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd_laurentNegPart, and TauCeti.HasLaurentSeriesOnAnnulus.tendsto_laurentNegPart_cocompact: convergence and analyticity of the positive part on Metric.eball c R and of the negative part on (Metric.closedBall c r)ᶜ, with vanishing at infinity.
• TauCeti.HasLaurentSeriesOnAnnulus.eq_laurentPosPart_add_laurentNegPart and TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd: Laurent splitting and analyticity of the sum on the open annulus.
• TauCeti.HasLaurentSeriesOnAnnulus.hasFPowerSeriesOnBall_update_of_neg_eq_zero: removable-singularity extension across c when negative coefficients vanish.

References

• John B. Conway, Functions of One Complex Variable I, Graduate Texts in Mathematics 11, Springer, 2nd edition, 1978, Chapter V, §1.
• Lars V. Ahlfors, Complex Analysis, 3rd edition, McGraw-Hill, 1979, Chapter 5, §1.2.

structure TauCeti.HasLaurentSeriesOnAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (a : ℤ → E) (c : ℂ) (r : ℝ) (R : ENNReal) : Prop

HasLaurentSeriesOnAnnulus f a c r R states that 0 ≤ r, ENNReal.ofReal r < R, and at every point w of the open concentric annulus Metric.eball c R \ Metric.closedBall c r the integer-indexed Laurent series ∑_{n ∈ ℤ} (w - c) ^ n • a n has sum f w.

When r = 0, Metric.closedBall c 0 = {c}, so the domain is the punctured open disk Metric.eball c R \ {c} (or the whole punctured plane ℂ \ {c} when R = ⊤).

• r_nonneg : 0 ≤ r

  The inner radius is nonnegative, excluding the center c from the open annulus.

• r_lt : ENNReal.ofReal r < R

  The open annulus is nonempty.

• hasSum {w : ℂ} : w ∈ Metric.eball c R \ Metric.closedBall c r → HasSum (fun (n : ℤ) => (w - c) ^ n • a n) (f w)

  Pointwise convergence of the integer-indexed Laurent series on the open annulus.

theorem TauCeti.hasLaurentSeriesOnAnnulus_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} : HasLaurentSeriesOnAnnulus f a c r R ↔ 0 ≤ r ∧ ENNReal.ofReal r < R ∧ ∀ ⦃w : ℂ⦄, w ∈ Metric.eball c R \ Metric.closedBall c r → HasSum (fun (n : ℤ) => (w - c) ^ n • a n) (f w)

Unbundled characterization of HasLaurentSeriesOnAnnulus.

theorem HasFPowerSeriesOnBall.hasLaurentSeriesOnAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {p : FormalMultilinearSeries ℂ ℂ E} {c : ℂ} {R : ENNReal} (hf : HasFPowerSeriesOnBall f p c R) : TauCeti.HasLaurentSeriesOnAnnulus f (fun (n : ℤ) => if 0 ≤ n then p.coeff n.toNat else 0) c 0 R

A formal power series expansion on Metric.eball c R restricts to a Laurent series expansion on the punctured disk Metric.eball c R \ Metric.closedBall c 0 whose negative-degree coefficients vanish and whose nonnegative-degree coefficients are p.coeff n.

noncomputable def TauCeti.laurentPosPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) : FormalMultilinearSeries ℂ ℂ E

The formal multilinear power series whose n-th coefficient is a n (n : ℕ), representing the nonnegative part of a Laurent series.

theorem TauCeti.laurentPosPowerSeries_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (n : ℕ) : laurentPosPowerSeries a n = ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ↑n)

Defining formula for the n-th term of laurentPosPowerSeries.

@[simp]

theorem TauCeti.coeff_laurentPosPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (n : ℕ) : (laurentPosPowerSeries a).coeff n = a ↑n

The n-th scalar coefficient of laurentPosPowerSeries a is a n.

theorem TauCeti.norm_laurentPosPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (n : ℕ) : ‖laurentPosPowerSeries a n‖ = ‖a ↑n‖

The operator norm of laurentPosPowerSeries a n equals ‖a n‖.

theorem TauCeti.laurentPosPowerSeries_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (n : ℕ) (y : ℂ) : ((laurentPosPowerSeries a n) fun (x : Fin n) => y) = y ^ n • a ↑n

Evaluating laurentPosPowerSeries a n on the constant tuple fun _ => y yields y ^ n • a n.

@[simp]

theorem TauCeti.laurentPosPowerSeries_circleLaurentCoeff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) : laurentPosPowerSeries (circleLaurentCoeff f c R) = cauchyPowerSeries f c R

For circle Laurent coefficients, laurentPosPowerSeries is literally Mathlib's cauchyPowerSeries.

noncomputable def TauCeti.laurentPosPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (c w : ℂ) : E

The nonnegative-degree sum ∑' n : ℕ, (w - c) ^ n • a n of a Laurent series.

theorem TauCeti.laurentPosPart_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (c w : ℂ) : laurentPosPart a c w = ∑' (n : ℕ), (w - c) ^ n • a ↑n

Defining series formula for laurentPosPart.

noncomputable def TauCeti.laurentNegPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (c w : ℂ) : E

The negative-degree (principal) sum ∑' n : ℕ, (w - c) ^ (-(n + 1)) • a (-(n + 1)) of a Laurent series.

theorem TauCeti.laurentNegPart_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (c w : ℂ) : laurentNegPart a c w = ∑' (n : ℕ), (w - c) ^ (-(↑n + 1)) • a (-(↑n + 1))

Defining series formula for laurentNegPart.

@[simp]

theorem TauCeti.laurentPosPart_at_center {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℤ → E) (c : ℂ) : laurentPosPart a c c = a 0

At the center c, laurentPosPart a c c evaluates to the constant term a 0.

theorem TauCeti.laurentNegPart_eq_zero_of_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a : ℤ → E} (ha : ∀ (k : ℕ), a (-(↑k + 1)) = 0) (c w : ℂ) : laurentNegPart a c w = 0

When all negative-degree Laurent coefficients vanish, laurentNegPart is identically zero.

theorem TauCeti.HasLaurentSeriesOnAnnulus.outerRadius_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : 0 < R

The outer radius of a convergent Laurent series on an open annulus is strictly positive.

theorem TauCeti.HasLaurentSeriesOnAnnulus.exists_radius {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : ∃ (ρ : ℝ), r < ρ ∧ ENNReal.ofReal ρ < R

Every convergent Laurent series on Metric.eball c R \ Metric.closedBall c r admits an interior circle radius ρ with r < ρ and ENNReal.ofReal ρ < R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r r' : ℝ} {R R' : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hr : r ≤ r') (hR : R' ≤ R) (hrR' : ENNReal.ofReal r' < R') : HasLaurentSeriesOnAnnulus f a c r' R'

Restriction of a Laurent series expansion to a concentric subannulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hfg : Set.EqOn f g (Metric.eball c R \ Metric.closedBall c r)) : HasLaurentSeriesOnAnnulus g a c r R

Functions agreeing on the open annulus share the same Laurent series expansions.

theorem TauCeti.HasLaurentSeriesOnAnnulus.zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) {r : ℝ} {R : ENNReal} (hr : 0 ≤ r) (hrR : ENNReal.ofReal r < R) : HasLaurentSeriesOnAnnulus (fun (x : ℂ) => 0) (fun (x : ℤ) => 0) c r R

The zero function has the zero Laurent series on any nonempty open annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {a b : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hf : HasLaurentSeriesOnAnnulus f a c r R) (hg : HasLaurentSeriesOnAnnulus g b c r R) : HasLaurentSeriesOnAnnulus (fun (w : ℂ) => f w + g w) (fun (n : ℤ) => a n + b n) c r R

Termwise addition of Laurent series on the same open annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hf : HasLaurentSeriesOnAnnulus f a c r R) : HasLaurentSeriesOnAnnulus (fun (w : ℂ) => -f w) (fun (n : ℤ) => -a n) c r R

Termwise negation of a Laurent series on an open annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {a b : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hf : HasLaurentSeriesOnAnnulus f a c r R) (hg : HasLaurentSeriesOnAnnulus g b c r R) : HasLaurentSeriesOnAnnulus (fun (w : ℂ) => f w - g w) (fun (n : ℤ) => a n - b n) c r R

Termwise subtraction of Laurent series on the same open annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hf : HasLaurentSeriesOnAnnulus f a c r R) (b : ℂ) : HasLaurentSeriesOnAnnulus (fun (w : ℂ) => b • f w) (fun (n : ℤ) => b • a n) c r R

Scalar multiplication of a Laurent series by a complex constant.

theorem TauCeti.HasLaurentSeriesOnAnnulus.sub_zpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (v : E) (c : ℂ) (m : ℤ) {r : ℝ} {R : ENNReal} (hr : 0 ≤ r) (hrR : ENNReal.ofReal r < R) : HasLaurentSeriesOnAnnulus (fun (w : ℂ) => (w - c) ^ m • v) (fun (n : ℤ) => if n = m then v else 0) c r R

A Laurent monomial (w - c) ^ m • v has the single-term Laurent expansion supported at m.

theorem TauCeti.HasLaurentSeriesOnAnnulus.le_radius_laurentPosPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : R ≤ (laurentPosPowerSeries a).radius

The radius of convergence of the nonnegative formal power series laurentPosPowerSeries a is at least the outer radius R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.summable_norm_mul_pow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) : Summable fun (n : ℕ) => ‖a ↑n‖ * ρ ^ n

Pointwise convergence of a Laurent series on an open annulus implies absolute norm-power summability of its nonnegative-degree terms on every interior circle of radius ρ ∈ (r, R).

theorem TauCeti.HasLaurentSeriesOnAnnulus.summable_norm_mul_zpow_neg_add_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) : Summable fun (n : ℕ) => ‖a (-(↑n + 1))‖ * ρ ^ (-(↑n + 1))

Pointwise convergence of a Laurent series on an open annulus implies absolute norm-power summability of its negative-degree terms on every interior circle of radius ρ ∈ (r, R).

theorem TauCeti.HasLaurentSeriesOnAnnulus.summable_norm_mul_zpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) : Summable fun (n : ℤ) => ‖a n‖ * ρ ^ n

Pointwise convergence of a Laurent series on an open annulus automatically yields absolute norm-power summability ∑_{n ∈ ℤ} ‖a n‖ * ρ ^ n < ∞ on every interior circle of radius ρ ∈ (r, R).

theorem TauCeti.HasLaurentSeriesOnAnnulus.exists_summable_norm_bound_on_closedAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r r' R' : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hrr' : r < r') (hr'R' : r' ≤ R') (hR'R : ENNReal.ofReal R' < R) : ∃ (B : ℤ → ℝ), Summable B ∧ ∀ (n : ℤ), ∀ w ∈ Metric.closedBall c R' \ Metric.ball c r', ‖(w - c) ^ n • a n‖ ≤ B n

On any closed concentric subannulus Metric.closedBall c R' \ Metric.ball c r' inside the open annulus, the Laurent terms admit a uniform summable norm majorant.

theorem TauCeti.HasLaurentSeriesOnAnnulus.tendstoUniformlyOn_closedAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r r' R' : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hrr' : r < r') (hr'R' : r' ≤ R') (hR'R : ENNReal.ofReal R' < R) : TendstoUniformlyOn (fun (t : Finset ℤ) (w : ℂ) => ∑ n ∈ t, (w - c) ^ n • a n) f Filter.atTop (Metric.closedBall c R' \ Metric.ball c r')

On any closed concentric subannulus inside the open annulus, the finite partial sums of the Laurent series converge uniformly to f.

theorem TauCeti.HasLaurentSeriesOnAnnulus.hasFPowerSeriesOnBall_laurentPosPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : HasFPowerSeriesOnBall (laurentPosPart a c) (laurentPosPowerSeries a) c R

The positive-degree part of a Laurent series on Metric.eball c R \ Metric.closedBall c r converges as a formal power series on the entire open disk Metric.eball c R, including at c.

theorem TauCeti.HasLaurentSeriesOnAnnulus.hasSum_laurentPosPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c w : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hw : w ∈ Metric.eball c R) : HasSum (fun (n : ℕ) => (w - c) ^ n • a ↑n) (laurentPosPart a c w)

The nonnegative part laurentPosPart a c has convergent series throughout Metric.eball c R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd_laurentPosPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : AnalyticOnNhd ℂ (laurentPosPart a c) (Metric.eball c R)

The nonnegative part laurentPosPart a c is complex-analytic on the entire disk Metric.eball c R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.differentiableOn_laurentPosPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : DifferentiableOn ℂ (laurentPosPart a c) (Metric.eball c R)

The nonnegative part laurentPosPart a c is complex-differentiable on the entire disk Metric.eball c R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.hasSum_laurentNegPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c w : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hw : w ∉ Metric.closedBall c r) : HasSum (fun (n : ℕ) => (w - c) ^ (-(↑n + 1)) • a (-(↑n + 1))) (laurentNegPart a c w)

The negative part laurentNegPart a c converges at every point outside Metric.closedBall c r (in particular on the whole punctured plane ℂ \ {c} when r = 0).

theorem TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd_laurentNegPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : AnalyticOnNhd ℂ (laurentNegPart a c) (Metric.closedBall c r)ᶜ

The negative part laurentNegPart a c is complex-analytic on (Metric.closedBall c r)ᶜ (the whole punctured plane ℂ \ {c} when r = 0).

theorem TauCeti.HasLaurentSeriesOnAnnulus.differentiableOn_laurentNegPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : DifferentiableOn ℂ (laurentNegPart a c) (Metric.closedBall c r)ᶜ

The negative part laurentNegPart a c is complex-differentiable on (Metric.closedBall c r)ᶜ.

theorem TauCeti.HasLaurentSeriesOnAnnulus.tendsto_laurentNegPart_cocompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : Filter.Tendsto (laurentNegPart a c) (Filter.cocompact ℂ) (nhds 0)

The negative part laurentNegPart a c vanishes at infinity (Filter.cocompact ℂ).

theorem TauCeti.HasLaurentSeriesOnAnnulus.eq_laurentPosPart_add_laurentNegPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c w : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (hw : w ∈ Metric.eball c R \ Metric.closedBall c r) : f w = laurentPosPart a c w + laurentNegPart a c w

On the open annulus, f splits as the sum of its nonnegative and negative Laurent parts.

theorem TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : AnalyticOnNhd ℂ f (Metric.eball c R \ Metric.closedBall c r)

Any function admitting a convergent Laurent series on an open annulus is complex-analytic on that annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : DifferentiableOn ℂ f (Metric.eball c R \ Metric.closedBall c r)

Any function admitting a convergent Laurent series on an open annulus is complex-differentiable on that annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) : ContinuousOn f (Metric.eball c R \ Metric.closedBall c r)

Any function admitting a convergent Laurent series on an open annulus is continuous on that annulus.

theorem TauCeti.HasLaurentSeriesOnAnnulus.eqOn_laurentPosPart_of_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c r R) (ha : ∀ (k : ℕ), a (-(↑k + 1)) = 0) : Set.EqOn f (laurentPosPart a c) (Metric.eball c R \ Metric.closedBall c r)

If all negative-degree coefficients vanish, a function with a Laurent series on an open annulus agrees on that annulus with its nonnegative-degree sum laurentPosPart a c.

theorem TauCeti.HasLaurentSeriesOnAnnulus.eqOn_update_laurentPosPart_of_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) (ha : ∀ (k : ℕ), a (-(↑k + 1)) = 0) : Set.EqOn (Function.update f c (a 0)) (laurentPosPart a c) (Metric.eball c R)

On a punctured disk (r = 0), if all negative-degree coefficients vanish, updating f at the center c with a 0 makes it agree with laurentPosPart a c on the whole disk Metric.eball c R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.hasFPowerSeriesOnBall_update_of_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) (ha : ∀ (k : ℕ), a (-(↑k + 1)) = 0) : HasFPowerSeriesOnBall (Function.update f c (a 0)) (laurentPosPowerSeries a) c R

Removable-singularity power series extension. If a convergent Laurent series on the punctured disk Metric.eball c R \ {c} has vanishing negative-degree coefficients, then Function.update f c (a 0) has the formal power series laurentPosPowerSeries a on all of Metric.eball c R.

theorem TauCeti.HasLaurentSeriesOnAnnulus.analyticOnNhd_update_of_neg_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) (ha : ∀ (k : ℕ), a (-(↑k + 1)) = 0) : AnalyticOnNhd ℂ (Function.update f c (a 0)) (Metric.eball c R)

If a convergent Laurent series on Metric.eball c R \ {c} has vanishing negative-degree coefficients, then Function.update f c (a 0) is complex-analytic on Metric.eball c R.