Documentation

TauCeti.Analysis.Complex.Laurent.Expansion

Laurent series expansion, uniqueness, removable singularities, and differentiation #

Let E be a complex normed space. Building on the two-circle Cauchy integral formula and radius invariance of TauCeti.circleLaurentCoeff from TauCeti.Analysis.Complex.Laurent.Basic together with TauCeti.HasLaurentSeriesOnAnnulus from TauCeti.Analysis.Complex.Laurent.Series, this file proves:

  1. Cauchy-Laurent geometric expansions on circles (without completeness): the nonnegative circle Laurent series on C(c, R) sums inside Metric.ball c R to the outer Cauchy integral, and the negative circle Laurent series on C(c, r) (0 < r) sums outside Metric.closedBall c r to minus the inner Cauchy integral, adapting Mathlib's hasSum_two_pi_I_cauchyPowerSeries_integral (by Yury Kudryashov) to the exterior of C(c, r).
  2. Coefficient extraction and uniqueness (for complete E): on every interior circle of radius ρ ∈ (r, R), circleLaurentCoeff f c ρ recovers the coefficients of any convergent Laurent series of f, so Laurent series coefficients on an open annulus are unique.
  3. Laurent's theorem (for complete E): every function continuous on an open concentric annulus Metric.eball c R \ Metric.closedBall c r (0 ≤ r, ENNReal.ofReal r < R, allowing r = 0 and R = ⊤) and complex-differentiable outside a countable subset admits a convergent Laurent series with coefficients circleLaurentCoeff f c ρ for any ρ ∈ (r, R).
  4. Removable-singularity characterization (for complete E): a convergent Laurent series on a punctured disk Metric.eball c R \ {c} agrees near c with a function analytic at c if and only if all negative-degree coefficients vanish.
  5. Term-by-term differentiation (for complete E): differentiating a convergent Laurent series shifts coefficients by n ↦ (n + 1) • a (n + 1).

Main results #

References #

Geometric series expansions of outer and inner Cauchy integrals #

source
theorem TauCeti.hasSum_circleLaurentCoeff_natCast {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c w : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) (hw : w ∈ Metric.ball c R) :
HasSum (fun (n : ℕ) => (w - c) ^ n • circleLaurentCoeff f c R ↑n) ((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z)

For any circle-integrable function f on C(c, R) and any w ∈ Metric.ball c R, the nonnegative circle Laurent series converges to the outer Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z.

source
theorem TauCeti.hasSum_circleIntegral_geometric_inv_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c w : ℂ} {r : ℝ} (hr : 0 < r) (hf : CircleIntegrable f c r) (hw : r < dist w c) :
HasSum (fun (n : ℕ) => ∮ (z : ℂ) in C(c, r), ((z - c) / (w - c)) ^ n • (w - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (w - z)⁻¹ • f z)

For any circle-integrable function f on C(c, r) (0 < r) and any w outside the closed disk Metric.closedBall c r, the geometric series expansion of (w - z)⁻¹ converges under the circle integral to ∮ z in C(c, r), (w - z)⁻¹ • f z.

source
theorem TauCeti.hasSum_circleLaurentCoeff_neg_add_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c w : ℂ} {r : ℝ} (hr : 0 < r) (hf : CircleIntegrable f c r) (hw : r < dist w c) :
HasSum (fun (n : ℕ) => (w - c) ^ (-(↑n + 1)) • circleLaurentCoeff f c r (-(↑n + 1))) (-((2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - w)⁻¹ • f z))

For any circle-integrable function f on C(c, r) (0 < r) and any w with r < dist w c, the negative-degree circle Laurent series converges to minus the inner Cauchy integral -((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, r), (z - w)⁻¹ • f z).

Coefficient extraction, uniqueness, and Laurent's theorem #

source
theorem TauCeti.circleLaurentCoeff_eq_of_hasSum_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hs : ∀ z ∈ Metric.sphere c ρ, HasSum (fun (k : ℤ) => (z - c) ^ k • a k) (f z)) (hnorm : Summable fun (k : ℤ) => ‖a k‖ * ρ ^ k) (n : ℤ) :
circleLaurentCoeff f c ρ n = a n

If ∑_{k ∈ ℤ} (z - c) ^ k • a k converges to f z on Metric.sphere c ρ (0 < ρ) with summable norm bounds ∑_{k ∈ ℤ} ‖a k‖ * ρ ^ k < ∞, then circleLaurentCoeff f c ρ n = a n for every n : ℤ.

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.circleLaurentCoeff_eq {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) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) (n : ℤ) :
circleLaurentCoeff f c ρ n = a n

Cauchy-Laurent coefficient formula. For any convergent Laurent series on Metric.eball c R \ Metric.closedBall c r and any interior circle radius ρ ∈ (r, R), the n-th Laurent coefficient is circleLaurentCoeff f c ρ n.

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.coeff_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a b : ℤ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (ha : HasLaurentSeriesOnAnnulus f a c r R) (hb : HasLaurentSeriesOnAnnulus f b c r R) :
a = b

Uniqueness of Laurent series coefficients. Two Laurent series converging to the same function on the same open annulus have identical coefficients.

source
theorem TauCeti.hasSum_circleLaurentCoeff_of_differentiable_on_annulus_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c w : ℂ} {r ρ R : ℝ} {s : Set ℂ} (hr : 0 < r) (hrρ : r ≤ ρ) (hρR : ρ ≤ R) (hs : s.Countable) (hw : w ∈ Metric.ball c R \ Metric.closedBall c r) (hc : ContinuousOn f (Metric.closedBall c R \ Metric.ball c r)) (hd : ∀ z ∈ (Metric.ball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) :
HasSum (fun (n : ℤ) => (w - c) ^ n • circleLaurentCoeff f c ρ n) (f w)

Pointwise Laurent expansion on a closed annulus. If f is continuous on the closed annulus Metric.closedBall c R \ Metric.ball c r (0 < r) and complex-differentiable outside a countable set in the open annulus, then at every w ∈ Metric.ball c R \ Metric.closedBall c r and for every integrating radius ρ ∈ [r, R], the Laurent series with coefficients circleLaurentCoeff f c ρ converges to f w.

source
theorem TauCeti.hasLaurentSeriesOnAnnulus_of_differentiable_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal} {s : Set ℂ} (hr : 0 ≤ r) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) (hs : s.Countable) (hc : ContinuousOn f (Metric.eball c R \ Metric.closedBall c r)) (hd : ∀ z ∈ (Metric.eball c R \ Metric.closedBall c r) \ s, DifferentiableAt ℂ f z) :
HasLaurentSeriesOnAnnulus f (circleLaurentCoeff f c ρ) c r R

Laurent's theorem on an open concentric annulus (with countable exceptional set). Let 0 ≤ r and r < ρ with ENNReal.ofReal ρ < R (allowing r = 0 for punctured disks and R = ⊤ for exteriors of closed disks or ℂ \ {c}). If f : ℂ → E is continuous on the open annulus Metric.eball c R \ Metric.closedBall c r and complex-differentiable outside a countable set s, then f has the convergent Laurent series with coefficients circleLaurentCoeff f c ρ throughout Metric.eball c R \ Metric.closedBall c r.

source
theorem DifferentiableOn.hasLaurentSeriesOnAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} {r ρ : ℝ} {R : ENNReal} (hf : DifferentiableOn ℂ f (Metric.eball c R \ Metric.closedBall c r)) (hr : 0 ≤ r) (hrρ : r < ρ) (hρR : ENNReal.ofReal ρ < R) :
TauCeti.HasLaurentSeriesOnAnnulus f (TauCeti.circleLaurentCoeff f c ρ) c r R

Laurent's theorem on an open concentric annulus. Every function f : ℂ → E into a complex Banach space that is complex-differentiable on Metric.eball c R \ Metric.closedBall c r (0 ≤ r, r < ρ, ENNReal.ofReal ρ < R) expands in a convergent Laurent series with coefficients circleLaurentCoeff f c ρ.

source
theorem TauCeti.differentiableOn_iff_exists_hasLaurentSeriesOnAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hr : 0 ≤ r) (hrR : ENNReal.ofReal r < R) :
DifferentiableOn ℂ f (Metric.eball c R \ Metric.closedBall c r) ↔ ∃ (a : ℤ → E), HasLaurentSeriesOnAnnulus f a c r R

For a complete target space E, complex differentiability on a nonempty open concentric annulus is equivalent to admitting a convergent Laurent series on that annulus.

source
theorem TauCeti.analyticOnNhd_iff_exists_hasLaurentSeriesOnAnnulus {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} {r : ℝ} {R : ENNReal} (hr : 0 ≤ r) (hrR : ENNReal.ofReal r < R) :
AnalyticOnNhd ℂ f (Metric.eball c R \ Metric.closedBall c r) ↔ ∃ (a : ℤ → E), HasLaurentSeriesOnAnnulus f a c r R

For a complete target space E, complex analyticity on a nonempty open concentric annulus is equivalent to admitting a convergent Laurent series on that annulus.

Removable-singularity characterization on punctured disks #

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.coeff_neg_add_one_eq_zero_of_analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f g : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) (hg : AnalyticAt ℂ g c) (hfg : f =ᶠ[nhdsWithin c {c}ᶜ] g) (k : ℕ) :
a (-(↑k + 1)) = 0

If f has a Laurent series on Metric.eball c R \ {c} and agrees on a punctured neighborhood of c with a function analytic at c, then all negative-degree coefficients of a vanish.

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.coeff_zero_eq_of_analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f g : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) (hg : AnalyticAt ℂ g c) (hfg : f =ᶠ[nhdsWithin c {c}ᶜ] g) :
a 0 = g c

If f has a Laurent series on Metric.eball c R \ {c} and agrees on a punctured neighborhood of c with a function g analytic at c, then a 0 = g c.

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.exists_analyticAt_eventuallyEq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {a : ℤ → E} {c : ℂ} {R : ENNReal} (h : HasLaurentSeriesOnAnnulus f a c 0 R) :
(∃ (g : ℂ → E), AnalyticAt ℂ g c ∧ f =ᶠ[nhdsWithin c {c}ᶜ] g) ↔ ∀ (k : ℕ), a (-(↑k + 1)) = 0

Characterization of removable singularities via Laurent coefficients. A function with a convergent Laurent series on Metric.eball c R \ {c} agrees on a punctured neighborhood of c with a function analytic at c if and only if all of its negative-degree coefficients vanish.

Term-by-term differentiation of Laurent series #

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.deriv {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) :
HasLaurentSeriesOnAnnulus (_root_.deriv f) (fun (n : ℤ) => ↑(n + 1) • a (n + 1)) c r R

Term-by-term differentiation of a convergent Laurent series. If f has the Laurent series with coefficients a on an open annulus, then deriv f has the Laurent series with coefficients n ↦ ((n + 1 : ℤ) : ℂ) • a (n + 1) on the same open annulus.

source
theorem TauCeti.HasLaurentSeriesOnAnnulus.hasSum_deriv {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) :
HasSum (fun (n : ℤ) => (↑n * (w - c) ^ (n - 1)) • a n) (_root_.deriv f w)

Unshifted term-by-term differentiation formula: on the open annulus, ∑_{n ∈ ℤ} (n * (w - c) ^ (n - 1)) • a n converges to deriv f w.