Reversal and concatenation of piecewise C¹ curves

The contour-integration layer works with raw curves γ : ℝ → ℂ on a parameter interval [[a, b]] (Contour.IsPiecewiseC1On) and with the raw contour integral ∫ t in a..b, deriv γ t • f (γ t). This file supplies the two operations on such curves that a path-independence argument needs: running a curve backwards, and following one curve by another.

• The reversal t ↦ γ (c - t) of a curve on [[a, b]] is a curve on [[c - a, c - b]]; its contour integral over a..b is the contour integral of γ over c - a..c - b. Taking c to be the sum of the endpoints of a second interval lets the reversed curve start where another curve ends.
• The concatenation t ↦ if t ≤ b then γ t else δ t of a curve γ on [a, b] and a curve δ on [b, c] that agree at b is piecewise C¹ on [a, c]. The contour integral only sees a curve on the open interior of its parameter interval, so it splits as the sum of the contour integrals of γ and δ.

Main results

• TauCeti.Contour.IsPiecewiseC1On.comp_const_sub — reversal preserves piecewise C¹ regularity.
• TauCeti.Contour.intervalIntegral_deriv_smul_comp_const_sub — the contour integral of the reversed curve.
• TauCeti.Contour.IsPiecewiseC1On.if_le — concatenation preserves piecewise C¹ regularity.
• TauCeti.Contour.intervalIntegral_deriv_smul_congr — the contour integral depends on the curve only through its values on the open parameter interval.
• TauCeti.Contour.intervalIntegral_deriv_smul_eq_add_of_eqOn — the contour integral along a concatenation is the sum of the contour integrals along its pieces.

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

Reversal of a piecewise-C¹ curve. If γ is piecewise C¹ on [[a, b]], then the reversed curve t ↦ γ (c - t) is piecewise C¹ on [[c - a, c - b]], with the reflected breakpoints.

theorem TauCeti.Contour.intervalIntegral_deriv_smul_comp_const_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (γ : ℝ → ℂ) (f : ℂ → E) (a b c : ℝ) : ∫ (t : ℝ) in a..b, deriv (fun (t : ℝ) => γ (c - t)) t • f (γ (c - t)) = ∫ (t : ℝ) in c - a..c - b, deriv γ t • f (γ t)

The contour integral along a reversed curve. The contour integral of t ↦ γ (c - t) over a..b is the contour integral of γ over c - a..c - b. In particular, for c = a + b the transformed endpoints are b and a, in reverse order, so it is ∫ t in b..a, deriv γ t • f (γ t), the negative of the contour integral of γ over a..b.

theorem TauCeti.Contour.IsPiecewiseC1On.if_le {γ δ : ℝ → ℂ} {a b c : ℝ} (h₁ : IsPiecewiseC1On γ a b) (h₂ : IsPiecewiseC1On δ b c) (hab : a ≤ b) (hbc : b ≤ c) (hb : γ b = δ b) : IsPiecewiseC1On (fun (t : ℝ) => if t ≤ b then γ t else δ t) a c

Concatenation of piecewise-C¹ curves. If γ is piecewise C¹ on [a, b], δ is piecewise C¹ on [b, c], and the two agree at b, then the curve following γ up to time b and δ afterwards is piecewise C¹ on [a, c].

theorem TauCeti.Contour.intervalIntegral_deriv_smul_congr {γ δ : ℝ → ℂ} {a b : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} (h : Set.EqOn γ δ (Set.uIoo a b)) : ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = ∫ (t : ℝ) in a..b, deriv δ t • f (δ t)

The contour integral sees only the open parameter interval. If two curves agree on the open interval between a and b, their contour integrals over a..b agree, even though the integrand involves the derivative of the curve.

theorem TauCeti.Contour.intervalIntegral_deriv_smul_eq_add_of_eqOn {γ δ : ℝ → ℂ} {a b c : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {η : ℝ → ℂ} (hγ : Set.EqOn η γ (Set.uIoo a b)) (hδ : Set.EqOn η δ (Set.uIoo b c)) (hγi : IntervalIntegrable (fun (t : ℝ) => deriv γ t • f (γ t)) MeasureTheory.volume a b) (hδi : IntervalIntegrable (fun (t : ℝ) => deriv δ t • f (δ t)) MeasureTheory.volume b c) : ∫ (t : ℝ) in a..c, deriv η t • f (η t) = (∫ (t : ℝ) in a..b, deriv γ t • f (γ t)) + ∫ (t : ℝ) in b..c, deriv δ t • f (δ t)

The contour integral along a concatenation. If η agrees with γ on the open interval between a and b and with δ on the open interval between b and c, and the contour integrands of γ and δ are integrable there, then the contour integral of η over a..c is the sum of those of γ over a..b and of δ over b..c. This applies in particular to the concatenation t ↦ if t ≤ b then γ t else δ t when a ≤ b ≤ c.