Circle Laurent coefficients and the two-circle Cauchy formula

The circle integral defining a Laurent coefficient is independent of its positive radius provided the function is continuous on the intervening closed annulus and complex differentiable outside a countable exceptional set in its open interior. Under the same hypotheses, the two-circle Cauchy formula represents the function between the circles by the difference of its outer and inner Cauchy integrals, even at exceptional points. Neither result assumes that the function extends across the center: isolated essential singularities are allowed. When f is complex-differentiable on a circle with circle-integrable derivative, integrating around the circle also expresses the Laurent coefficients of deriv f in terms of those of f (circleLaurentCoeff_deriv_of_differentiableAt, circleLaurentCoeff_deriv).

The construction uses Mathlib's Cauchy-Goursat theorem for annuli, Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable, and its removable divided difference dslope. These are the integral ingredients for splitting a Laurent expansion into its positive and negative parts. The divided-difference proof of the two-circle formula is adapted from Mathlib's Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux, by Yury Kudryashov, from a disc to an annulus. To include exceptional evaluation points, we reuse Mathlib's local power-series theorem, whose Cauchy formula extends to those points by continuity and closure.

For the classical Cauchy and Laurent formulas, see John B. Conway, Functions of One Complex Variable I, Chapters IV (Complex Integration) and V (Singularities).

noncomputable def TauCeti.circleLaurentCoeff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℤ) : E

The coefficient of degree n extracted by a circle of radius R centered at c. For functions continuous on a closed annulus and complex differentiable outside a countable set in its interior, circleLaurentCoeff_eq_of_differentiable_on_annulus_off_countable makes this independent of the choice of circle within that annulus.

theorem TauCeti.circleLaurentCoeff_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℤ) : circleLaurentCoeff f c R n = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-n - 1) • f z

The circle-integral formula for the integer-indexed Laurent coefficient.

theorem TauCeti.circleLaurentCoeff_natCast {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) : circleLaurentCoeff f c R ↑n = (cauchyPowerSeries f c R).coeff n

The nonnegative Laurent coefficients are exactly the coefficients of Mathlib's Cauchy power series, even for the degenerate circle of radius zero.

theorem TauCeti.circleLaurentCoeff_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hfg : Set.EqOn f g (Metric.sphere c R)) (n : ℤ) : circleLaurentCoeff f c R n = circleLaurentCoeff g c R n

Coefficient extraction depends only on the values on the integrating circle.

@[simp]

theorem TauCeti.circleLaurentCoeff_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (c : ℂ) (R : ℝ) (n : ℤ) : circleLaurentCoeff (fun (x : ℂ) => 0) c R n = 0

Every coefficient of the zero function vanishes.

@[simp]

theorem TauCeti.circleLaurentCoeff_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (a : ℂ) (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℤ) : circleLaurentCoeff (fun (z : ℂ) => a • f z) c R n = a • circleLaurentCoeff f c R n

Extracting coefficients commutes with complex scalar multiplication.

theorem TauCeti.circleLaurentCoeff_sub_zpow_smul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ) (m n : ℤ) : circleLaurentCoeff (fun (z : ℂ) => (z - c) ^ m • f z) c R n = circleLaurentCoeff f c R (n - m)

Multiplying a function by (z - c) ^ m shifts its coefficients by m: the coefficient of degree n of (z - c) ^ m • f z is the coefficient of degree n - m of f.

theorem TauCeti.circleLaurentCoeff_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) (n : ℤ) : circleLaurentCoeff (fun (z : ℂ) => f z + g z) c R n = circleLaurentCoeff f c R n + circleLaurentCoeff g c R n

Extracting coefficients is additive for functions integrable on the circle.

theorem TauCeti.norm_circleLaurentCoeff_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R M : ℝ} (hR : 0 ≤ R) (hf : ∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ M) (n : ℤ) : ‖circleLaurentCoeff f c R n‖ ≤ M * R ^ (-n)

The Cauchy estimate for any integer Laurent coefficient, including negative degrees and the degenerate circle of radius zero.

theorem TauCeti.circleLaurentCoeff_eq_of_differentiable_on_annulus_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) {s : Set ℂ} (hs : s.Countable) (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) (n : ℤ) : circleLaurentCoeff f c R n = circleLaurentCoeff f c r n

The Laurent coefficient does not change when a circle moves through a closed annulus on which the function is continuous and complex differentiable away from a countable exceptional set in the open annulus.

theorem TauCeti.circleLaurentCoeff_eq_of_differentiable_on_open_annulus_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {r ρ₁ ρ₂ : ℝ} {R : ENNReal} {s : Set ℂ} (hr : 0 ≤ r) (hr₁ : r < ρ₁) (hr₂ : r < ρ₂) (hR₁ : ENNReal.ofReal ρ₁ < R) (hR₂ : 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) (n : ℤ) : circleLaurentCoeff f c ρ₁ n = circleLaurentCoeff f c ρ₂ n

On an open concentric annulus Metric.eball c R \ Metric.closedBall c r, any two interior radii ρ₁, ρ₂ ∈ (r, R) yield identical circleLaurentCoeff values when f is continuous on the open annulus and complex-differentiable outside a countable subset.

@[simp]

theorem TauCeti.circleLaurentCoeff_sub_zpow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (a : E) (c : ℂ) {R : ℝ} (hR : 0 < R) (m n : ℤ) : circleLaurentCoeff (fun (z : ℂ) => (z - c) ^ m • a) c R n = if n = m then a else 0

A Laurent monomial has precisely its prescribed coefficient, in every integer degree.

theorem TauCeti.circleIntegral_dslope_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c w : ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ) (hf : CircleIntegrable f c ρ) (hw : w ∉ Metric.sphere c ρ) : ∮ (z : ℂ) in C(c, ρ), dslope f w z = (∮ (z : ℂ) in C(c, ρ), (z - w)⁻¹ • f z) - (∮ (z : ℂ) in C(c, ρ), (z - w)⁻¹) • f w

The circle integral of the divided difference dslope f w around a circle avoiding w is the difference of the Cauchy integral of f and the circle integral of (z - w)⁻¹ times f w. Only integrability of f on the circle is needed.

theorem TauCeti.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_sub_of_differentiable_on_annulus_off_countable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c w : ℂ} {r R : ℝ} (hr : 0 < r) {s : Set ℂ} (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) : (2 * ↑Real.pi * Complex.I)⁻¹ • ((∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - w)⁻¹ • f z) = f w

The two-circle Cauchy formula on an annulus. The function is continuous on the closed annulus and complex differentiable outside a countable exceptional set in the open annulus. The evaluation point may belong to the exceptional set.

theorem TauCeti.circleLaurentCoeff_deriv_of_differentiableAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 < R) (hd : ∀ z ∈ Metric.sphere c R, DifferentiableAt ℂ f z) (hderiv : CircleIntegrable (deriv f) c R) (n : ℤ) : circleLaurentCoeff (deriv f) c R n = ↑(n + 1) • circleLaurentCoeff f c R (n + 1)

If f is complex-differentiable at every point of Metric.sphere c R (0 < R) and deriv f is circle-integrable on C(c, R), then the n-th circle Laurent coefficient of deriv f equals (n + 1) • circleLaurentCoeff f c R (n + 1).

theorem TauCeti.circleLaurentCoeff_deriv {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) (n : ℤ) : circleLaurentCoeff (deriv f) c ρ n = ↑(n + 1) • circleLaurentCoeff f c ρ (n + 1)

For f complex-differentiable on an open concentric annulus Metric.eball c R \ Metric.closedBall c r and any interior circle radius ρ ∈ (r, R), the n-th circle Laurent coefficient of deriv f equals (n + 1) • circleLaurentCoeff f c ρ (n + 1).