Documentation

TauCeti.Analysis.Contour.Winding.SegmentSum

The index integral as a sum of segment logarithm increments #

Given a monotone partition a = s 0 ≤ ⋯ ≤ s N = b fine enough that on each segment the normalized ratio (γ t - w) / (γ (s j) - w) stays in Complex.slitPlane, the logarithmic-derivative integral splits into a sum of per-segment logarithm increments:

∫ t in a..b, γ' t / (γ t - w) = ∑ j < N, Complex.log ((γ (s (j+1)) - w) / (γ (s j) - w)).

Specializing γ' = deriv γ and rewriting γ' t / (γ t - w) as the winding integrand (γ t - w)⁻¹ * deriv γ t gives the form consumed by the winding-number computation. The per-segment slit-plane hypothesis is exactly the data the continuous argument-lift partition supplies, so this evaluation bridges that partition to the winding-number computation: it is the first half of showing the winding number of a closed curve is an integer, since for a closed curve the real parts of these increments telescope away and the imaginary parts sum to the total argument change.

Main results #

Provenance #

Adapted from contourIntegral_inv_eq_sum_log_segRatio in WindingArgDiff.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on [a, b].

source
theorem TauCeti.Contour.integral_deriv_div_sub_eq_sum_log {γ γ' : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} {N : ℕ} {s : ℕ → ℝ} (hP : P.Countable) (hs_zero : s 0 = a) (hs_N : s N = b) (hs_mono : Monotone s) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b \ P, HasDerivAt γ (γ' t) t) (h_slit : ∀ j < N, ∀ t ∈ Set.Icc (s j) (s (j + 1)), (γ t - w) / (γ (s j) - w) ∈ Complex.slitPlane) (h_int : IntervalIntegrable (fun (t : ℝ) => γ' t / (γ t - w)) MeasureTheory.volume a b) :
∫ (t : ℝ) in a..b, γ' t / (γ t - w) = ∑ j ∈ Finset.range N, Complex.log ((γ (s (j + 1)) - w) / (γ (s j) - w))

Index integral as a sum of segment logarithm increments. For a monotone partition a = s 0 ≤ ⋯ ≤ s N = b of [a, b] with γ continuous there, differentiable with derivative γ' off a countable set P, and with the normalized segment ratio (γ t - w) / (γ (s j) - w) in Complex.slitPlane on each [s j, s (j+1)], the integral of γ' t / (γ t - w) equals the sum of the per-segment Complex.log increments.

source
theorem TauCeti.Contour.integral_inv_sub_mul_deriv_eq_sum_log {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} {N : ℕ} {s : ℕ → ℝ} (hP : P.Countable) (hs_zero : s 0 = a) (hs_N : s N = b) (hs_mono : Monotone s) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b \ P, DifferentiableAt ℝ γ t) (h_slit : ∀ j < N, ∀ t ∈ Set.Icc (s j) (s (j + 1)), (γ t - w) / (γ (s j) - w) ∈ Complex.slitPlane) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) :
∫ (t : ℝ) in a..b, (γ t - w)⁻¹ * deriv γ t = ∑ j ∈ Finset.range N, Complex.log ((γ (s (j + 1)) - w) / (γ (s j) - w))

Winding-integrand form. The γ' = deriv γ specialization of integral_deriv_div_sub_eq_sum_log with the winding integrand (γ t - w)⁻¹ * deriv γ t, as consumed by the winding-number computation.

source
theorem TauCeti.Contour.integral_deriv_div_sub_eq_log_norm_add_I_mul_sum_log_im {γ γ' : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} {N : ℕ} {s : ℕ → ℝ} (hP : P.Countable) (hs_zero : s 0 = a) (hs_N : s N = b) (hs_mono : Monotone s) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b \ P, HasDerivAt γ (γ' t) t) (h_slit : ∀ j < N, ∀ t ∈ Set.Icc (s j) (s (j + 1)), (γ t - w) / (γ (s j) - w) ∈ Complex.slitPlane) (h_int : IntervalIntegrable (fun (t : ℝ) => γ' t / (γ t - w)) MeasureTheory.volume a b) :
∫ (t : ℝ) in a..b, γ' t / (γ t - w) = ↑(Real.log ‖γ b - w‖ - Real.log ‖γ a - w‖) + Complex.I * ↑(∑ j ∈ Finset.range N, (Complex.log ((γ (s (j + 1)) - w) / (γ (s j) - w))).im)

Real/imaginary decomposition of the index integral (explicit velocity). Refining integral_deriv_div_sub_eq_sum_log, over the same slit-compatible monotone partition the integral of γ' t / (γ t - w) splits into a real logarithm-of-modulus increment Real.log ‖γ b - w‖ - Real.log ‖γ a - w‖ plus I times the imaginary part of the segment logarithm sum. For a closed curve the real increment vanishes, isolating the total argument change.

source
theorem TauCeti.Contour.integral_inv_sub_mul_deriv_eq_log_norm_add_I_mul_sum_log_im {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} {N : ℕ} {s : ℕ → ℝ} (hP : P.Countable) (hs_zero : s 0 = a) (hs_N : s N = b) (hs_mono : Monotone s) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Ioo a b \ P, DifferentiableAt ℝ γ t) (h_slit : ∀ j < N, ∀ t ∈ Set.Icc (s j) (s (j + 1)), (γ t - w) / (γ (s j) - w) ∈ Complex.slitPlane) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) :
∫ (t : ℝ) in a..b, (γ t - w)⁻¹ * deriv γ t = ↑(Real.log ‖γ b - w‖ - Real.log ‖γ a - w‖) + Complex.I * ↑(∑ j ∈ Finset.range N, (Complex.log ((γ (s (j + 1)) - w) / (γ (s j) - w))).im)

Winding-integrand form of the index-integral decomposition. The γ' = deriv γ specialization of integral_deriv_div_sub_eq_log_norm_add_I_mul_sum_log_im, stated with the winding integrand (γ t - w)⁻¹ * deriv γ t, as consumed by the closed-curve winding-number computation.

source
theorem TauCeti.Contour.re_integral_inv_sub_mul_deriv_eq_log_norm {γ : ℝ → ℂ} {s : ℂ} {l u : ℝ} {P : Set ℝ} (hlu : l ≤ u) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.Icc l u)) (hγ_diff : ∀ t ∈ Set.Ioo l u \ P, DifferentiableAt ℝ γ t) (h_ne : ∀ t ∈ Set.Icc l u, γ t ≠ s) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume l u) :
(∫ (t : ℝ) in l..u, (γ t - s)⁻¹ * deriv γ t).re = Real.log ‖γ u - s‖ - Real.log ‖γ l - s‖

The real part of the plain-piece contour integral telescopes to the log-norm difference of its endpoints, with no slit-plane hypothesis needed: taking real parts of integral_inv_sub_mul_deriv_eq_log_norm_add_I_mul_sum_log_im's decomposition discards its imaginary sum term (a real number times Complex.I), leaving exactly the log-norm difference, independent of any branch choice on the partition exists_continuousOn_arg_lift_with_partition supplies.