Strict monotonicity of the distance to a crossed point

Near a transverse crossing — γ t₀ = s with non-zero one-sided derivative limit L, for a curve γ : ℝ → F into a real inner product space — the distance ‖γ t - s‖ is strictly monotone on a one-sided closed interval at t₀: increasing to the right, decreasing to the left. Consequently the curve exits each small disc around s exactly once on each side, which is what lets the crossing analysis of the generalized residue theorem invert ε ↦ exit time and build the excision cutoffs of the principal value.

The mechanism: (d/dt)‖γ t - s‖² = 2⟪γ t - s, deriv γ t⟫_ℝ, whose leading term (t - t₀)‖L‖² dominates the differentiation errors on a small one-sided interval.

Main results

• Contour.exists_strictMonoOn_norm_sub_right — ‖γ t - s‖ is strictly increasing on [t₀, t₀ + r] for some r > 0.
• Contour.exists_strictAntiOn_norm_sub_left — ‖γ t - s‖ is strictly decreasing on [t₀ - r, t₀] for some r > 0.

Provenance

Migrated from norm_sub_strictMonoOn_right and norm_sub_strictAntiOn_left of CrossingDataBuilder.lean in the AINTLIB LeanModularForms development, restated for a raw curve (there the eventual differentiability comes from a bundled ClosedPwC1Immersion); the left lemma is derived from the right one by the reflection t ↦ 2t₀ - t instead of repeating the argument. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.exists_strictMonoOn_norm_sub_right {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {γ : ℝ → F} {t₀ : ℝ} {s : F} (h_at : γ t₀ = s) {L : F} (hL : L ≠ 0) (hL_right : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L)) (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t) : ∃ r > 0, StrictMonoOn (fun (t : ℝ) => ‖γ t - s‖) (Set.Icc t₀ (t₀ + r))

The distance to a crossed point is strictly increasing to the right of the crossing: for a curve through s = γ t₀ with non-zero right derivative limit L, continuity at t₀, and eventual differentiability on the right, ‖γ t - s‖ is strictly monotone on [t₀, t₀ + r] for some r > 0 — the curve exits each small disc around s exactly once.

theorem TauCeti.Contour.exists_strictAntiOn_norm_sub_left {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {γ : ℝ → F} {t₀ : ℝ} {s : F} (h_at : γ t₀ = s) {L : F} (hL : L ≠ 0) (hL_left : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L)) (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t) : ∃ r > 0, StrictAntiOn (fun (t : ℝ) => ‖γ t - s‖) (Set.Icc (t₀ - r) t₀)

The distance to a crossed point is strictly decreasing to the left of the crossing: the counterpart of exists_strictMonoOn_norm_sub_right, derived from it by the reflection t ↦ 2t₀ - t (which carries the left data of γ to right data of the reflected curve with derivative limit -L).