Piecewise C¹ curves on an interval

The contour-integration roadmap states its objects — the generalized winding number, the contour integral, and the Hungerbühler--Wasem regularity conditions — for a piecewise C¹ curve γ : ℝ → ℂ on the closed interval [[a, b]] between two parameters (in either order): continuous there, and C¹ on each piece between finitely many breakpoints. This file introduces that regularity as a predicate Contour.IsPiecewiseC1On γ a b on the raw function γ itself — following the roadmap's function-based design, with no bundled path type — together with its API.

The predicate is the regularity a "regularity package" will use to discharge the integrand-level hypotheses — continuity, pointwise differentiability, and integrability — that the raw contour-integral lemmas take directly. Those lemmas do not consume the predicate themselves: the fundamental theorem of calculus along a contour in Contour.ArcFTC, for instance, is stated on the integrand so it works with any regularity package that supplies these hypotheses. The predicate is a prerequisite for the homology Cauchy theorem and the generalized residue theorem.

Main definitions

• Contour.IsPiecewiseC1On γ a b — γ is continuous on [[a, b]] and C¹ on every closed subinterval whose interior avoids a fixed finite breakpoint set in (min a b, max a b).

Main results

• Contour.isPiecewiseC1On_iff — unfold the predicate to its defining clauses.
• Contour.IsPiecewiseC1On.continuousOn — the underlying continuity on [[a, b]].
• Contour.IsPiecewiseC1On.of_contDiffOn — a C¹ curve is piecewise C¹, with no breakpoints.
• Contour.IsPiecewiseC1On.of_breakpoints, Contour.IsPiecewiseC1On.exists_breakpoints — introduce the predicate from, and eliminate it to, a finite breakpoint witness.
• Contour.IsPiecewiseC1On.mono — restrict the regularity to a subinterval [[c, d]] ⊆ [[a, b]].
• Contour.isPiecewiseC1On_comm, Contour.IsPiecewiseC1On.symm — endpoint-swap invariance.
• Contour.IsPiecewiseC1On.add, Contour.IsPiecewiseC1On.sub, Contour.IsPiecewiseC1On.const_smul — the predicate is stable under the vector-space operations on curves, the two breakpoint sets being merged by union.
• Contour.IsPiecewiseC1On.exists_finset_differentiableAt, Contour.IsPiecewiseC1On.exists_countable_differentiableAt — differentiability off a finite (hence countable) set, in the exact shapes the raw contour-integral lemmas consume.
• Contour.IsPiecewiseC1On.eventually_differentiableAt (and its _right/_left one-sided corollaries) — eventual differentiability near an interior parameter.
• Contour.IsPiecewiseC1On.intervalIntegrable_deriv — the derivative is interval-integrable on a..b, glued across the breakpoints from the C¹ pieces.
• Contour.IsPiecewiseC1On.isBounded_image_deriv — the derivative has bounded image on [[a, b]], glued the same way.

Provenance

Adapted from the regularity fields of the PiecewiseC1PathOn structure in the AINTLIB LeanModularForms development, re-expressed as a predicate on a raw function γ : ℝ → ℂ per the roadmap's function-based contour design rather than as a bundled path type. The piece-level integrability of the derivative and its gluing across the breakpoints (IsPiecewiseC1On.intervalIntegrable_deriv) follow ClosedPwC1Curve.deriv_intervalIntegrable_piece and ClosedPwC1Curve.deriv_extend_intervalIntegrable in the same development's PaperPwC1Immersion.lean, restated for the raw curve.

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

Piecewise C¹ on the interval between a and b. The curve γ : ℝ → ℂ is continuous on the closed interval [[a, b]] (unordered, hence orientation-robust), and there is a finite set of breakpoints p ⊆ (min a b, max a b) such that γ is C¹ on every closed subinterval of [[a, b]] whose interior avoids p. Equivalently γ is continuously differentiable on each piece between consecutive breakpoints, with corners allowed only at the breakpoints; an unbounded-derivative cusp such as t ↦ √|t| is excluded, being not C¹ up to the breakpoint. This is the raw-function form of the roadmap's piecewise-C¹ curve — a Prop on γ itself, with no bundled path type.

Equations

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

theorem TauCeti.Contour.isPiecewiseC1On_iff {γ : ℝ → ℂ} {a b : ℝ} : IsPiecewiseC1On γ a b ↔ ContinuousOn γ (Set.uIcc a b) ∧ ∃ (p : Finset ℝ), ↑p ⊆ Set.Ioo (min a b) (max a b) ∧ ∀ (c d : ℝ), Set.Icc c d ⊆ Set.uIcc a b → Disjoint (↑p) (Set.Ioo c d) → ContDiffOn ℝ 1 γ (Set.Icc c d)

IsPiecewiseC1On 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.

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

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

theorem TauCeti.Contour.IsPiecewiseC1On.of_contDiffOn {γ : ℝ → ℂ} {a b : ℝ} (h : ContDiffOn ℝ 1 γ (Set.uIcc a b)) : IsPiecewiseC1On γ a b

A C¹ curve on [[a, b]] is piecewise C¹, with no breakpoints.

theorem TauCeti.Contour.IsPiecewiseC1On.of_breakpoints {γ : ℝ → ℂ} {a b : ℝ} (hcont : ContinuousOn γ (Set.uIcc a b)) (p : Finset ℝ) (hp : ↑p ⊆ Set.Ioo (min a b) (max a b)) (hC1 : ∀ (c d : ℝ), Set.Icc c d ⊆ Set.uIcc a b → Disjoint (↑p) (Set.Ioo c d) → ContDiffOn ℝ 1 γ (Set.Icc c d)) : IsPiecewiseC1On γ a b

Build a piecewise-C¹ curve from continuity on [[a, b]] together with a finite breakpoint set off which every breakpoint-free closed subinterval carries a C¹ restriction.

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

Extract the finite breakpoint set of a piecewise-C¹ curve, together with the C¹ restriction it induces on every breakpoint-free closed subinterval of [[a, b]].

theorem TauCeti.Contour.IsPiecewiseC1On.mono {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) {c d : ℝ} (hsub : Set.uIcc c d ⊆ Set.uIcc a b) : IsPiecewiseC1On γ c d

Piecewise-C¹ regularity restricts to any subinterval: if γ is piecewise C¹ on [[a, b]] and [[c, d]] ⊆ [[a, b]], then γ is piecewise C¹ on [[c, d]], with the breakpoint set cut down to the smaller interior.

theorem TauCeti.Contour.isPiecewiseC1On_comm {γ : ℝ → ℂ} {a b : ℝ} : IsPiecewiseC1On γ a b ↔ IsPiecewiseC1On γ b a

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

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

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

theorem TauCeti.Contour.IsPiecewiseC1On.add {a b : ℝ} {γ₁ γ₂ : ℝ → ℂ} (h₁ : IsPiecewiseC1On γ₁ a b) (h₂ : IsPiecewiseC1On γ₂ a b) : IsPiecewiseC1On (fun (t : ℝ) => γ₁ t + γ₂ t) a b

A sum of piecewise-C¹ curves is piecewise C¹, with the union of the two breakpoint sets as breakpoints: a closed subinterval whose interior avoids the union avoids each set separately, so both summands are C¹ there.

theorem TauCeti.Contour.IsPiecewiseC1On.sub {a b : ℝ} {γ₁ γ₂ : ℝ → ℂ} (h₁ : IsPiecewiseC1On γ₁ a b) (h₂ : IsPiecewiseC1On γ₂ a b) : IsPiecewiseC1On (fun (t : ℝ) => γ₁ t - γ₂ t) a b

A difference of piecewise-C¹ curves is piecewise C¹.

theorem TauCeti.Contour.IsPiecewiseC1On.const_smul {γ : ℝ → ℂ} {a b : ℝ} (c : ℝ) (h : IsPiecewiseC1On γ a b) : IsPiecewiseC1On (fun (t : ℝ) => c • γ t) a b

A real scalar multiple of a piecewise-C¹ curve is piecewise C¹, with the same breakpoints.

theorem TauCeti.Contour.exists_Icc_subset_uIcc_disjoint {a b : ℝ} {s : Set ℝ} (hs : IsClosed s) {t : ℝ} (ht : t ∈ Set.Ioo (min a b) (max a b)) (hts : t ∉ s) : ∃ (c : ℝ) (d : ℝ), t ∈ Set.Ioo c d ∧ Set.Icc c d ⊆ Set.uIcc a b ∧ Disjoint s (Set.Ioo c d)

Around any interior parameter outside a closed set s there is a closed subinterval of [[a, b]] whose interior contains t and is disjoint from s.

theorem TauCeti.Contour.IsPiecewiseC1On.exists_finset_differentiableAt {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) : ∃ (p : Finset ℝ), ∀ t ∈ Set.Ioo (min a b) (max a b) \ ↑p, DifferentiableAt ℝ γ t

Differentiability off a finite set. A piecewise-C¹ curve is differentiable at every interior parameter outside a finite set — the breakpoints.

theorem TauCeti.Contour.IsPiecewiseC1On.exists_countable_differentiableAt {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) : ∃ (P : Set ℝ), P.Countable ∧ ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t

Differentiability off a countable set. A piecewise-C¹ curve is differentiable at every interior parameter outside a countable set — the breakpoints. This is the exact regularity shape consumed by the raw contour-integral development (Dixon's argument and the winding-number machinery).

theorem TauCeti.Contour.IsPiecewiseC1On.eventually_differentiableAt {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (min a b) (max a b)) {u : Set ℝ} (hu : t₀ ∉ u) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ u, DifferentiableAt ℝ γ t

Eventual differentiability near an interior parameter, on any within-filter avoiding the parameter itself.

theorem TauCeti.Contour.IsPiecewiseC1On.eventually_differentiableAt_right {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (min a b) (max a b)) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t

Eventual differentiability from the right at an interior parameter.

theorem TauCeti.Contour.IsPiecewiseC1On.eventually_differentiableAt_left {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (min a b) (max a b)) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t

Eventual differentiability from the left at an interior parameter.

theorem TauCeti.Contour.IsPiecewiseC1On.intervalIntegrable_deriv {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b

Interval-integrability of the derivative. The derivative of a piecewise-C¹ curve is interval-integrable on a..b: on each piece the within-derivative is continuous on a compact interval and agrees with deriv almost everywhere, and the pieces glue across the finitely many breakpoints. This discharges the hderiv_int hypothesis of the raw contour-integral lemmas.

theorem TauCeti.Contour.IsPiecewiseC1On.isBounded_image_deriv {γ : ℝ → ℂ} {a b : ℝ} (h : IsPiecewiseC1On γ a b) : Bornology.IsBounded (deriv γ '' Set.uIcc a b)

Boundedness of the derivative of a piecewise-C¹ curve on its whole parameter interval. Mirrors IsPiecewiseC1On.intervalIntegrable_deriv's gluing-across-breakpoints argument, but for boundedness of the image rather than interval-integrability. Orientation-generic like its sibling: unlike Icc a b, which is empty (not Icc b a) when b < a, uIcc a b is symmetric in a and b, so no a ≤ b hypothesis is needed.