Documentation

TauCeti.Analysis.Contour.Argument.Lift

Continuous argument lift for a point-avoiding curve #

For a curve γ : ℝ → ℂ continuous on [a, b] and avoiding a point w, the function t ↦ γ t - w is nowhere zero there, so on [a, b] it admits a real-valued argument lift θ, continuous on [a, b], with γ t - w = ‖γ t - w‖ · exp (i θ t) for t ∈ [a, b]. This is the geometric heart of the integer-valuedness of the generalized winding number: for a closed curve the total argument change θ b - θ a is an integer multiple of 2π.

The lift is built on a partition a = s₀ ≤ ⋯ ≤ s_N = b fine enough that each segment ratio (γ t - w) / (γ (s j) - w) stays within distance 1/2 of 1, hence in Complex.slitPlane, where Complex.log extracts a single-valued argument; the segment contributions telescope to the global lift.

Mathlib's Complex.exists_continuousOn_eqOn_exp_comp already gives a continuous logarithm (hence argument) branch for a nowhere-zero continuous function on a simply connected open set. The explicit partition-and-segRatio construction here is retained because the downstream winding-number integral is evaluated segment by segment, which needs the partition data that the bare-existence API does not expose.

Main results #

Provenance #

Adapted from WindingInteger.lean in the AINTLIB LeanModularForms development. Prerequisite for the integer-valuedness and local constancy of the generalized winding number, hence for the homology Cauchy theorem (roadmap homologyCauchyTheorem) and the generalized residue theorem.

Partition lemma #

Segment-ratio helpers #

The continuous argument lift below is assembled from a partition of [a, b]: on each segment the ratio (γ t - w) / (γ (s j) - w) lies within distance 1/2 of 1, hence in Complex.slitPlane (via Mathlib's Complex.ball_one_subset_slitPlane), where Complex.log extracts a single-valued argument; the Im (log ·) contributions telescope across the partition. The definitions and lemmas supporting that construction follow.

source
noncomputable def TauCeti.Contour.segRatio (γ : ℝ → ℂ) (w : ℂ) (s_j s_jp1 t : ℝ) :
ℂ

The segment ratio (γ (segClamp s_j s_jp1 t) - w) / (γ s_j - w): on the partition segment [s_j, s_{j+1}] it measures γ t - w against its value at the left endpoint s_j, held constant in t outside the segment. Summing the Complex.logs of these ratios over a partition yields a continuous argument lift of t ↦ γ t - w.

Equations
Instances For
    source
    theorem TauCeti.Contour.segRatio_eq_one_of_le {γ : ℝ → ℂ} {w : ℂ} {s_j s_jp1 t : ℝ} (ht : t ≤ s_j) (h_ne : γ s_j - w ≠ 0) :
    segRatio γ w s_j s_jp1 t = 1

    Before its segment (t ≤ s_j), the segment ratio equals 1.

    source
    theorem TauCeti.Contour.segRatio_eq_div_of_mem_Icc {γ : ℝ → ℂ} {w : ℂ} {s_j s_jp1 t : ℝ} (ht : t ∈ Set.Icc s_j s_jp1) :
    segRatio γ w s_j s_jp1 t = (γ t - w) / (γ s_j - w)

    On its segment (t ∈ [s_j, s_{j+1}]), the segment ratio is (γ t - w) / (γ s_j - w) — the primary meaning of segRatio.

    source
    theorem TauCeti.Contour.segRatio_eq_endpoint_div_of_le {γ : ℝ → ℂ} {w : ℂ} {s_j s_jp1 t : ℝ} (h : s_j ≤ s_jp1) (ht : s_jp1 ≤ t) :
    segRatio γ w s_j s_jp1 t = (γ s_jp1 - w) / (γ s_j - w)

    After its segment (s_{j+1} ≤ t), the segment ratio equals the full endpoint ratio (γ s_{j+1} - w) / (γ s_j - w).

    Telescoping product over a partition #

    Continuous arg-lift summand (continued) #

    The unit direction in polar form #

    source
    theorem TauCeti.Contour.div_norm_eq_exp_arg_mul_I {w : ℂ} (hw : w ≠ 0) :
    w / ↑‖w‖ = Complex.exp (↑w.arg * Complex.I)

    A nonzero complex number over its norm is the exponential of its argument: w / ↑‖w‖ = exp(arg w · I).

    source
    theorem TauCeti.Contour.exp_mul_I_congr_angle {x y : ℝ} (h : ↑x = ↑y) :
    Complex.exp (↑x * Complex.I) = Complex.exp (↑y * Complex.I)

    Two real representatives of the same Real.Angle have the same unit complex exponential. This is the coercion bridge from the quotient-valued angle API to complex polar form.

    Polar form of a product #

    Covering segment #

    Uniform partition with bounded mesh #

    Main theorem: argument lift on [a, b] #

    source
    theorem TauCeti.Contour.exists_continuousOn_arg_lift_with_partition {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (h_avoid : ∀ t ∈ Set.Icc a b, γ t ≠ w) :
    ∃ (N : ℕ) (s : ℕ → ℝ), 0 < N ∧ s 0 = a ∧ s N = b ∧ Monotone s ∧ (∀ j ≤ N, s j ∈ Set.Icc a b) ∧ (∀ j ≤ N, γ (s j) - w ≠ 0) ∧ (∀ j < N, ∀ t ∈ Set.Icc (s j) (s (j + 1)), (γ t - w) / (γ (s j) - w) ∈ Complex.slitPlane) ∧ ContinuousOn (fun (t : ℝ) => (γ a - w).arg + ∑ j ∈ Finset.range N, (Complex.log (segRatio γ w (s j) (s (j + 1)) t)).im) (Set.Icc a b) ∧ ∀ t ∈ Set.Icc a b, γ t - w = ↑‖γ t - w‖ * Complex.exp (Complex.I * ↑((γ a - w).arg + ∑ j ∈ Finset.range N, (Complex.log (segRatio γ w (s j) (s (j + 1)) t)).im))

    Argument lift on [a, b], with a partition. For γ continuous on [a, b] (a ≤ b) and avoiding w, there is a monotone partition a = s 0 ≤ ⋯ ≤ s N = b and a real function θ t = arg (γ a - w) + ∑_{j < N} (log (segRatio γ w (s j) (s (j+1)) t)).im, continuous on [a, b], satisfying γ t - w = ‖γ t - w‖ · exp (I · θ t) there. Each node has γ (s j) ≠ w, and on each segment j the ratio (γ t - w) / (γ (s j) - w) lies in Complex.slitPlane.