Piecewise C¹ immersions on an interval

The on-cycle Layer 4 targets of the contour-integration roadmap — the Hungerbühler–Wasem generalized residue theorem and its half-residue specialisation — are stated for a piecewise C¹ immersion: a piecewise-C¹ curve whose within-piece derivative is non-vanishing on every closed piece, one-sided at the piece endpoints. This file introduces that regularity as the predicate Contour.IsPwC1ImmersionOn γ a b on the raw function γ — the roadmap's pinned definition, verbatim — together with its basic API.

The non-vanishing tangent is what the on-cycle theory needs and the plain IsPiecewiseC1On cannot supply: Hungerbühler–Wasem represent each on-cycle singularity by model sectors of a definite opening angle, which requires a well-defined non-zero tangent there. The one-sided conditions are load-bearing: merely asking deriv γ ≠ 0 off a finite set would admit zero-speed turnarounds (γ t = t ^ 2 on [-1, 1], whose one-sided tangents both vanish at 0) and zero-speed seams of a closed curve, which are not immersions. derivWithin is used because at a corner the global deriv is 0 by Mathlib convention, which would falsely contradict non-vanishing; at interior points of a piece it agrees with deriv. (The homology Cauchy theorem, whose singularities lie off the curve, needs only IsPiecewiseC1On.)

Main definitions

• Contour.IsPwC1ImmersionOn γ a b — over a common finite breakpoint set, every breakpoint-free closed subinterval of [[a, b]] carries a C¹ restriction with non-vanishing within-piece derivative.

Main results

• Contour.isPwC1ImmersionOn_iff — unfold the predicate to its defining clauses.
• Contour.IsPwC1ImmersionOn.isPiecewiseC1On — an immersion is in particular piecewise C¹, with the same breakpoint witness.
• Contour.IsPwC1ImmersionOn.continuousOn — the underlying continuity on [[a, b]].
• Contour.IsPwC1ImmersionOn.of_breakpoints, Contour.IsPwC1ImmersionOn.exists_breakpoints — introduce the predicate from, and eliminate it to, a finite breakpoint witness.
• Contour.isPwC1ImmersionOn_comm, Contour.IsPwC1ImmersionOn.symm — endpoint-swap invariance.
• Contour.IsPwC1ImmersionOn.derivWithin_ne_zero_right, Contour.IsPwC1ImmersionOn.derivWithin_ne_zero_left — a crossing's one-sided velocity is non-zero on any window ending or starting there, from the immersion alone.
• Contour.IsPwC1ImmersionOn.exists_lipschitzOnWith_derivWithin_shrink_right, Contour.IsPwC1ImmersionOn.exists_lipschitzOnWith_derivWithin_shrink_left — shrink a one-sided Lipschitz-derivative window to fit inside a breakpoint-free piece the immersion supplies, picking up differentiability there for free.
• Contour.IsPwC1ImmersionOn.exists_deriv_slope_right_limit, Contour.IsPwC1ImmersionOn.exists_deriv_slope_left_limit — the same one-sided tangent as the limit of both deriv γ and the chord slope (γ t - γ t₀) / (t - t₀); the chord form is what the crossing angle needs.
• Contour.IsPwC1ImmersionOn.exists_deriv_right_limit, Contour.IsPwC1ImmersionOn.exists_deriv_left_limit — the tangent-limit projections of exists_deriv_slope_right_limit and exists_deriv_slope_left_limit.

Provenance

The raw-function mirror of the ClosedPwC1Immersion structure of the AINTLIB LeanModularForms development (PaperPwC1Immersion.lean): the pieces clause matches its contDiffOn_pieces and derivWithin_ne_zero_pieces fields — Hungerbühler–Wasem's Λ̇|_{[aₖ,aₖ₊₁]} ≠ 0 (arXiv:1808.00997, p. 3) — whose closed partition includes the interval endpoints, so the seam of a closed curve is constrained too. Closedness itself (γ a = γ b) stays a separate hypothesis of the theorems. The definition is pinned in the roadmap (TauCetiRoadmap/ContourIntegration/Suggested.lean).

def TauCeti.Contour.IsPwC1ImmersionOn (γ : ℝ → ℂ) (a b : ℝ) : Prop

Piecewise-C¹ immersion on the interval between a and b. The curve γ : ℝ → ℂ is continuous on [[a, b]] and, over a common finite breakpoint set p ⊆ (min a b, max a b), every breakpoint-free closed subinterval [c, d] carries a C¹ restriction whose within-piece derivative is non-vanishing on all of [c, d] — one-sided at the piece endpoints, including at a and b. This strengthens IsPiecewiseC1On by a non-vanishing tangent on every piece (IsPwC1ImmersionOn.isPiecewiseC1On); the c < d guard excludes degenerate pieces, on which derivWithin is not meaningful.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Contour.isPwC1ImmersionOn_iff {γ : ℝ → ℂ} {a b : ℝ} : IsPwC1ImmersionOn γ a b ↔ ContinuousOn γ (Set.uIcc a b) ∧ ∃ (p : Finset ℝ), ↑p ⊆ Set.Ioo (min a b) (max a b) ∧ ∀ (c d : ℝ), c < d → Set.Icc c d ⊆ Set.uIcc a b → Disjoint (↑p) (Set.Ioo c d) → ContDiffOn ℝ 1 γ (Set.Icc c d) ∧ ∀ t ∈ Set.Icc c d, derivWithin γ (Set.Icc c d) t ≠ 0

IsPwC1ImmersionOn unfolded to its defining clauses: continuity on [[a, b]], and a finite breakpoint set off which every breakpoint-free closed subinterval carries a C¹ restriction with non-vanishing within-piece derivative.

theorem TauCeti.Contour.IsPwC1ImmersionOn.continuousOn {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) : ContinuousOn γ (Set.uIcc a b)

A piecewise-C¹ immersion is continuous on the parameter interval [[a, b]].

theorem TauCeti.Contour.IsPwC1ImmersionOn.of_breakpoints {γ : ℝ → ℂ} {a b : ℝ} (hcont : ContinuousOn γ (Set.uIcc a b)) (p : Finset ℝ) (hp : ↑p ⊆ Set.Ioo (min a b) (max a b)) (hpieces : ∀ (c d : ℝ), c < d → Set.Icc c d ⊆ Set.uIcc a b → Disjoint (↑p) (Set.Ioo c d) → ContDiffOn ℝ 1 γ (Set.Icc c d) ∧ ∀ t ∈ Set.Icc c d, derivWithin γ (Set.Icc c d) t ≠ 0) : IsPwC1ImmersionOn γ a b

Build a piecewise-C¹ immersion from continuity on [[a, b]] together with a finite breakpoint set off which every breakpoint-free closed subinterval carries a C¹ restriction with non-vanishing within-piece derivative.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_breakpoints {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) : ∃ (p : Finset ℝ), ↑p ⊆ Set.Ioo (min a b) (max a b) ∧ ∀ (c d : ℝ), c < d → Set.Icc c d ⊆ Set.uIcc a b → Disjoint (↑p) (Set.Ioo c d) → ContDiffOn ℝ 1 γ (Set.Icc c d) ∧ ∀ t ∈ Set.Icc c d, derivWithin γ (Set.Icc c d) t ≠ 0

Extract the finite breakpoint set of a piecewise-C¹ immersion, together with the C¹ restriction and the non-vanishing within-piece derivative it induces on every breakpoint-free closed subinterval of [[a, b]].

theorem TauCeti.Contour.IsPwC1ImmersionOn.isPiecewiseC1On {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) : IsPiecewiseC1On γ a b

A piecewise-C¹ immersion is in particular piecewise C¹, with the same breakpoint witness.

theorem TauCeti.Contour.isPwC1ImmersionOn_comm {γ : ℝ → ℂ} {a b : ℝ} : IsPwC1ImmersionOn γ a b ↔ IsPwC1ImmersionOn γ b a

Piecewise-C¹-immersion regularity is symmetric in the endpoints, since [[a, b]] = [[b, a]].

theorem TauCeti.Contour.IsPwC1ImmersionOn.symm {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) : IsPwC1ImmersionOn γ b a

Piecewise-C¹-immersion regularity is invariant under swapping the endpoints of the interval.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_Icc_piece_right {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ico (min a b) (max a b)) : ∃ (d : ℝ), t₀ < d ∧ Set.Icc t₀ d ⊆ Set.uIcc a b ∧ ContDiffOn ℝ 1 γ (Set.Icc t₀ d) ∧ ∀ t ∈ Set.Icc t₀ d, derivWithin γ (Set.Icc t₀ d) t ≠ 0

The piece to the right of a parameter: every t₀ ∈ [min, max) begins a breakpoint-free closed piece [t₀, d] ⊆ [[a, b]] on which the immersion is C¹ with non-vanishing within-piece derivative.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_Icc_piece_left {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioc (min a b) (max a b)) : ∃ c < t₀, Set.Icc c t₀ ⊆ Set.uIcc a b ∧ ContDiffOn ℝ 1 γ (Set.Icc c t₀) ∧ ∀ t ∈ Set.Icc c t₀, derivWithin γ (Set.Icc c t₀) t ≠ 0

The piece to the left of a parameter: every t₀ ∈ (min, max] ends a breakpoint-free closed piece [c, t₀] ⊆ [[a, b]] on which the immersion is C¹ with non-vanishing within-piece derivative.

theorem TauCeti.Contour.IsPwC1ImmersionOn.derivWithin_ne_zero_right {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t d : ℝ} (ht₀ : t ∈ Set.Ico (min a b) (max a b)) (htd : t < d) : derivWithin γ (Set.Icc t d) t ≠ 0

A crossing's one-sided velocity is non-zero, from the immersion alone. No need to assume this alongside a C^{1,1} window at a crossing: IsPwC1ImmersionOn already forces a non-zero derivWithin-derivative at every point of the breakpoint-free piece to the right of t (IsPwC1ImmersionOn.exists_Icc_piece_right), including at t itself, and derivWithin at t does not depend on which (C¹ on [t, d]) right-piece it is computed against, since both agree with the same HasDerivWithinAt witness on their common initial segment.

theorem TauCeti.Contour.IsPwC1ImmersionOn.derivWithin_ne_zero_left {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {c t : ℝ} (ht₀ : t ∈ Set.Ioc (min a b) (max a b)) (hct : c < t) : derivWithin γ (Set.Icc c t) t ≠ 0

A crossing's one-sided velocity is non-zero, from the immersion alone, from the left. The mirror of IsPwC1ImmersionOn.derivWithin_ne_zero_right above.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_lipschitzOnWith_derivWithin_shrink_right {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ D : ℝ} {K : NNReal} (ht₀ : t₀ ∈ Set.Ico (min a b) (max a b)) (htD : t₀ < D) (hlip : LipschitzOnWith K (derivWithin γ (Set.Icc t₀ D)) (Set.Icc t₀ D)) : ∃ (d : ℝ), t₀ < d ∧ d < D ∧ DifferentiableOn ℝ γ (Set.Icc t₀ d) ∧ LipschitzOnWith K (derivWithin γ (Set.Icc t₀ d)) (Set.Icc t₀ d)

Shrinking a one-sided Lipschitz-derivative window to fit inside a breakpoint-free piece, from the right. If derivWithin γ is K-Lipschitz on [t₀, D], the immersion supplies a smaller [t₀, d] ⊆ [t₀, D] on which γ is differentiable and derivWithin γ is the same K-Lipschitz function -- not merely a restriction of the wider one, since derivWithin a priori depends on the underlying set. Away from the shared right endpoint d, both windows agree with the ordinary two-sided deriv γ directly (derivWithin_of_mem_nhds); at d itself, d is kept strictly inside a further breakpoint-free piece the immersion supplies, so γ has an honest two-sided derivative there too, and both windows' derivWithin again equal it.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_lipschitzOnWith_derivWithin_shrink_left {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {c t₀ : ℝ} {K : NNReal} (ht₀ : t₀ ∈ Set.Ioc (min a b) (max a b)) (hct : c < t₀) (hlip : LipschitzOnWith K (derivWithin γ (Set.Icc c t₀)) (Set.Icc c t₀)) : ∃ (d : ℝ), c < d ∧ d < t₀ ∧ DifferentiableOn ℝ γ (Set.Icc d t₀) ∧ LipschitzOnWith K (derivWithin γ (Set.Icc d t₀)) (Set.Icc d t₀)

The mirror of IsPwC1ImmersionOn.exists_lipschitzOnWith_derivWithin_shrink_right, from the left.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_deriv_slope_right_limit {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ico (min a b) (max a b)) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L) ∧ Filter.Tendsto (slope γ t₀) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L)

Non-zero one-sided tangent of an immersion, from the right. At every parameter t₀ ∈ [min, max) a piecewise-C¹ immersion has a non-zero limit of deriv γ from the right — the within-piece derivative there — and the chord slope (γ t - γ t₀) / (t - t₀) converges from the right to the same value.

Both limits are stated together, and about one L, because they are the same tangent: the derivative form is what the flatness conditions are stated against, while the chord form is what the direction of γ t - z₀ at a crossing is computed from. Splitting them into two existentials would lose the fact that they agree.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_deriv_right_limit {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ico (min a b) (max a b)) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L)

The tangent-limit half of IsPwC1ImmersionOn.exists_deriv_slope_right_limit.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_deriv_slope_left_limit {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioc (min a b) (max a b)) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L) ∧ Filter.Tendsto (slope γ t₀) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L)

Non-zero one-sided tangent of an immersion, from the left. The left-hand companion of IsPwC1ImmersionOn.exists_deriv_slope_right_limit: at every parameter t₀ ∈ (min, max] both deriv γ and the chord slope converge from the left to the same non-zero within-piece derivative.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_deriv_left_limit {γ : ℝ → ℂ} {a b : ℝ} (h : IsPwC1ImmersionOn γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioc (min a b) (max a b)) : ∃ (L : ℂ), L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L)

The tangent-limit half of IsPwC1ImmersionOn.exists_deriv_slope_left_limit.