Integrability of contour integrands

A piecewise-C¹ curve has interval-integrable derivative. Multiplying that derivative by a continuous function along the compact curve image therefore gives an interval-integrable contour integrand. This file packages that Layer 0 conclusion of the contour-integration roadmap for vector-valued integrands over ℂ.

The main theorem assumes continuity on the exact image γ '' [[a, b]]; a companion form accepts continuity on any set containing that image.

Main results

• IsPiecewiseC1On.intervalIntegrable_deriv_smul_comp — t ↦ deriv γ t • f (γ t) is interval-integrable when f is continuous on the curve image.
• IsPiecewiseC1On.intervalIntegrable_deriv_smul_comp_of_mapsTo — the same conclusion from continuity on an ambient set containing the curve.

The proof uses Mathlib's IntervalIntegrable.smul_continuousOn, after IsPiecewiseC1On.intervalIntegrable_deriv supplies integrability of the velocity.

theorem TauCeti.Contour.IsPiecewiseC1On.intervalIntegrable_deriv_smul_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {γ : ℝ → ℂ} {f : ℂ → E} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hf : ContinuousOn f (γ '' Set.uIcc a b)) : IntervalIntegrable (fun (t : ℝ) => deriv γ t • f (γ t)) MeasureTheory.volume a b

Along a piecewise-C¹ curve, the product of the curve velocity with a function continuous on the curve image is interval-integrable. This is the vector-valued contour integrand t ↦ deriv γ t • f (γ t) from Layer 0 of the contour-integration roadmap.

theorem TauCeti.Contour.IsPiecewiseC1On.intervalIntegrable_deriv_smul_comp_of_mapsTo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {γ : ℝ → ℂ} {f : ℂ → E} {a b : ℝ} {s : Set ℂ} (hγ : IsPiecewiseC1On γ a b) (hf : ContinuousOn f s) (hγs : Set.MapsTo γ (Set.uIcc a b) s) : IntervalIntegrable (fun (t : ℝ) => deriv γ t • f (γ t)) MeasureTheory.volume a b

Ambient-set form of IsPiecewiseC1On.intervalIntegrable_deriv_smul_comp: it suffices for f to be continuous on a set s containing the curve image.