Immersions are flat of order one

A piecewise-C¹ immersion is FlatOfOrder γ t₀ 1 at every interior parameter, and FlatOfOrderBasepoint γ a b 1 across the join: the curve leaves each point first-order tangent to its non-zero one-sided tangent, so the perpendicular deviation from the tangent line is o(‖γ t - γ t₀‖). This discharges the flatness clauses of Contour.ConditionAprime at simple poles for immersed cycles — together with IsPwC1ImmersionOn.finite_crossings it makes (A′) at simple poles a theorem about immersions rather than a hypothesis.

Main results

• Contour.IsPwC1ImmersionOn.flatOfOrder_one — an immersion is flat of order 1 at every interior parameter.
• Contour.IsPwC1ImmersionOn.flatOfOrderBasepoint_one — an immersion is flat of order 1 across the basepoint join.

Provenance

Migrated from isFlatOfOrder_one of FlatnessConditions.lean in the AINTLIB LeanModularForms development, restated for the raw curve on [[a, b]]: the one-sided derivatives recovered there from tendsto limits are here the within-piece derivatives of IsPwC1ImmersionOn at the piece endpoints. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3 (condition (A′) at simple poles).

theorem TauCeti.Contour.IsPwC1ImmersionOn.flatOfOrder_one {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (min a b) (max a b)) : FlatOfOrder γ t₀ 1

An immersion is flat of order one at every interior parameter (HW condition (A′) at a simple pole): the curve is first-order tangent to its non-zero one-sided tangents, so the perpendicular deviation from each tangent line is o(‖γ t - γ t₀‖).

theorem TauCeti.Contour.IsPwC1ImmersionOn.flatOfOrderBasepoint_one {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) (hab : a < b) : FlatOfOrderBasepoint γ a b 1

An immersion is flat of order one across the basepoint join (a < b): the outgoing branch at a and the incoming branch at b are each first-order tangent to their non-zero one-sided tangents.