Chord-quotient asymptotics at a transverse crossing

For a curve γ : ℝ → ℂ through a pole s = γ t₀ with non-vanishing one-sided derivative L, the chord quotient (γ t - s) / (t - t₀) tends to L, so on a small one-sided interval the normalized chord (γ t - s) / (L (t - t₀)) is close to 1. Two consequences feed the principal-value existence argument at the crossing:

• chord quotients (γ b - s) / (γ a - s) for a, b on a common side lie in Complex.slitPlane — the hypothesis under which the logarithmic fundamental theorem of calculus (Contour.integral_inv_sub_mul_deriv_eq_log) applies on the excised pieces;
• the arguments of the annular quotients converge as the excision cutoff δ(ε) → 0⁺, which pins the angle contribution of each branch at the pole.

Where the two sides share a proof, the statement is parametrised over the within-set u (Ioi t₀ on the right, Iio t₀ on the left).

Main results

• Contour.chord_quotient_tendsto — (γ t - s) / (t - t₀) → L along 𝓝[u] t₀ for t₀ ∉ u.
• Contour.exists_normalized_chord_bound_right / _left — ‖(γ t - s)/(L(t - t₀)) - 1‖ ≤ ρ on a fixed one-sided interval.
• Contour.div_mem_slitPlane_of_close_to_one — z / w ∈ slitPlane for z, w 1/4-close to 1.
• Contour.exists_chord_quotient_mem_slitPlane_right / _left — chord quotients on a small one-sided interval lie in the slit plane.
• Contour.arg_annular_quotient_tendsto_right / _left — convergence of the annular quotient arguments along a positive cutoff δ(ε) → 0⁺.
• Contour.exists_chord_div_tangent_mem_slitPlane_right / Contour.exists_neg_tangent_div_chord_mem_slitPlane_left — a window radius on which the boundary quotients (chord over tangent on the right, negated tangent over chord on the left) lie in the slit plane, discharging the h_slit hypotheses of the annular lemmas.
• Contour.exists_crossing_slitPlane_radius — the per-crossing package: one radius carrying all four slit-plane properties together with the non-zero one-sided derivatives, ready for a common minimum across the crossings of a pole.

Provenance

Migrated from chord_div_t_tendsto, normalized_chord_close, exists_normalized_chord_*, div_mem_slitPlane_of_close_to_one, chord_quotient_mem_slitPlane, exists_slitPlane_chord_quotient_*, tendsto_arg_of_pos_smul_tendsto, and arg_*_annular_tendsto of CPVExistence.lean, together with exists_chord_div_endpoint_slitPlane_right/_left of LocalCutoffs.lean, in the AINTLIB LeanModularForms development. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.chord_quotient_tendsto {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} {u : Set ℝ} (hu : t₀ ∉ u) (h_deriv : HasDerivWithinAt γ L u t₀) (h_at : γ t₀ = s) : Filter.Tendsto (fun (t : ℝ) => (γ t - s) / ↑(t - t₀)) (nhdsWithin t₀ u) (nhds L)

Chord-to-tangent quotient limit. Given HasDerivWithinAt γ L u t₀ with t₀ ∉ u and γ t₀ = s, the chord quotient (γ t - s) / (t - t₀) tends to L along 𝓝[u] t₀. Specialises to the one-sided limits at u = Ioi t₀ (right) and u = Iio t₀ (left).

theorem TauCeti.Contour.exists_normalized_chord_bound_right {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) {ρ : ℝ} (hρ_pos : 0 < ρ) : ∃ r > 0, ∀ t ∈ Set.Ioc t₀ (t₀ + r), ‖(γ t - s) / (L * ↑(t - t₀)) - 1‖ ≤ ρ

Fixed-radius normalized chord bound (right side): a positive radius r on whose right interval (t₀, t₀ + r] the normalized chord is uniformly ρ-close to 1.

theorem TauCeti.Contour.exists_normalized_chord_bound_left {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) {ρ : ℝ} (hρ_pos : 0 < ρ) : ∃ r > 0, ∀ t ∈ Set.Ico (t₀ - r) t₀, ‖(γ t - s) / (L * ↑(t - t₀)) - 1‖ ≤ ρ

Fixed-radius normalized chord bound (left side): the counterpart of exists_normalized_chord_bound_right on [t₀ - r, t₀).

theorem TauCeti.Contour.div_mem_slitPlane_of_close_to_one {z w : ℂ} (hz : ‖z - 1‖ ≤ 1 / 4) (hw : ‖w - 1‖ ≤ 1 / 4) : z / w ∈ Complex.slitPlane

Slit-plane condition for quotients near 1. If ‖z - 1‖ ≤ 1/4 and ‖w - 1‖ ≤ 1/4, then z / w ∈ Complex.slitPlane: the quotient stays in the unit ball around 1.

theorem TauCeti.Contour.chord_quotient_mem_slitPlane {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (hL : L ≠ 0) {a b : ℝ} (ha : ‖(γ a - s) / (L * ↑(a - t₀)) - 1‖ ≤ 1 / 4) (hb : ‖(γ b - s) / (L * ↑(b - t₀)) - 1‖ ≤ 1 / 4) (hab : 0 < (b - t₀) / (a - t₀)) : (γ b - s) / (γ a - s) ∈ Complex.slitPlane

Chord quotient in the slit plane (algebraic core). If the normalized chords at a and b are 1/4-close to 1 and a, b lie on a common side of t₀ — so that (b - t₀) / (a - t₀) > 0 — then (γ b - s) / (γ a - s) ∈ Complex.slitPlane.

theorem TauCeti.Contour.exists_chord_quotient_mem_slitPlane_right {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) : ∃ r > 0, ∀ (a b : ℝ), t₀ < a → a ≤ b → b ≤ t₀ + r → (γ b - s) / (γ a - s) ∈ Complex.slitPlane

Chord quotients on a small right interval lie in the slit plane: there is r > 0 such that (γ b - s) / (γ a - s) ∈ Complex.slitPlane whenever t₀ < a ≤ b ≤ t₀ + r.

theorem TauCeti.Contour.exists_chord_quotient_mem_slitPlane_left {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) : ∃ r > 0, ∀ (a b : ℝ), t₀ - r ≤ a → a ≤ b → b < t₀ → (γ b - s) / (γ a - s) ∈ Complex.slitPlane

Chord quotients on a small left interval lie in the slit plane: there is r > 0 such that (γ b - s) / (γ a - s) ∈ Complex.slitPlane whenever t₀ - r ≤ a ≤ b < t₀. Stated with a the left endpoint — the form in which the argument-lift fundamental theorem of calculus consumes it on the left excised piece.

theorem TauCeti.Contour.arg_tendsto_of_pos_mul_tendsto {α : Type u_1} {l : Filter α} {c : α → ℝ} {f : α → ℂ} {Q : ℂ} (hQ : Q ∈ Complex.slitPlane) (hc : ∀ᶠ (ε : α) in l, 0 < c ε) (h : Filter.Tendsto (fun (ε : α) => ↑(c ε) * f ε) l (nhds Q)) : Filter.Tendsto (fun (ε : α) => (f ε).arg) l (nhds Q.arg)

Positive real scaling does not move the argument: if Q ∈ slitPlane, c ε > 0 eventually, and (c ε : ℂ) * f ε → Q, then arg (f ε) → arg Q.

theorem TauCeti.Contour.arg_annular_quotient_tendsto_right {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) (h_at : γ t₀ = s) {δ : ℝ → ℝ} {r : ℝ} (h_slit : (γ (t₀ + r) - s) / L ∈ Complex.slitPlane) (hδ_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < δ ε) (hδ_to_zero : Filter.Tendsto δ (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))) : Filter.Tendsto (fun (ε : ℝ) => ((γ (t₀ + r) - s) / (γ (t₀ + δ ε) - s)).arg) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((γ (t₀ + r) - s) / L).arg)

Right annular quotient argument convergence: along a positive cutoff δ(ε) → 0⁺, the argument of the annular quotient (γ (t₀ + r) - s) / (γ (t₀ + δ ε) - s) converges to the argument of (γ (t₀ + r) - s) / L.

theorem TauCeti.Contour.arg_annular_quotient_tendsto_left {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) (h_at : γ t₀ = s) {δ : ℝ → ℝ} {r : ℝ} (h_slit : -L / (γ (t₀ - r) - s) ∈ Complex.slitPlane) (hδ_pos : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), 0 < δ ε) (hδ_to_zero : Filter.Tendsto δ (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0))) : Filter.Tendsto (fun (ε : ℝ) => ((γ (t₀ - δ ε) - s) / (γ (t₀ - r) - s)).arg) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-L / (γ (t₀ - r) - s)).arg)

Left annular quotient argument convergence: along a positive cutoff δ(ε) → 0⁺, the argument of the annular quotient (γ (t₀ - δ ε) - s) / (γ (t₀ - r) - s) converges to the argument of (-L) / (γ (t₀ - r) - s).

theorem TauCeti.Contour.exists_chord_div_tangent_mem_slitPlane_right {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) : ∃ r > 0, ∀ (r' : ℝ), 0 < r' → r' ≤ r → (γ (t₀ + r') - s) / L ∈ Complex.slitPlane

Boundary chord-to-tangent quotients in the slit plane (right): there is a window radius r > 0 such that (γ (t₀ + r') - s) / L ∈ Complex.slitPlane for every 0 < r' ≤ r — the h_slit input of arg_annular_quotient_tendsto_right at any admissible window radius.

theorem TauCeti.Contour.exists_neg_tangent_div_chord_mem_slitPlane_left {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) (h_at : γ t₀ = s) (hL : L ≠ 0) : ∃ r > 0, ∀ (r' : ℝ), 0 < r' → r' ≤ r → -L / (γ (t₀ - r') - s) ∈ Complex.slitPlane

Boundary chord-to-tangent quotients in the slit plane (left): there is a window radius r > 0 such that (-L) / (γ (t₀ - r') - s) ∈ Complex.slitPlane for every 0 < r' ≤ r — the h_slit input of arg_annular_quotient_tendsto_left at any admissible window radius.

theorem TauCeti.Contour.exists_crossing_slitPlane_radius {γ : ℝ → ℂ} {t₀ : ℝ} {s L_R L_L : ℂ} (h_deriv_R : HasDerivWithinAt γ L_R (Set.Ioi t₀) t₀) (h_deriv_L : HasDerivWithinAt γ L_L (Set.Iio t₀) t₀) (h_at : γ t₀ = s) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0) : ∃ r > 0, (∀ (a b : ℝ), t₀ < a → a ≤ b → b ≤ t₀ + r → (γ b - s) / (γ a - s) ∈ Complex.slitPlane) ∧ (∀ (a b : ℝ), t₀ - r ≤ a → a ≤ b → b < t₀ → (γ b - s) / (γ a - s) ∈ Complex.slitPlane) ∧ (∀ (r' : ℝ), 0 < r' → r' ≤ r → (γ (t₀ + r') - s) / L_R ∈ Complex.slitPlane) ∧ ∀ (r' : ℝ), 0 < r' → r' ≤ r → -L_L / (γ (t₀ - r') - s) ∈ Complex.slitPlane

The per-crossing slit-plane radius package: at a transverse crossing with non-zero one-sided derivatives, a single radius r > 0 carries all four slit-plane properties — the two-sided chord quotients and the two boundary tangent quotients at every admissible offset — so a common minimum over the crossings of a pole inherits them all.