Henstock–Kurzweil substitution with countably many singularities

A continuous scalar parametrization differentiable outside a countable exceptional set gives the usual substitution formula for a continuous Banach-valued integrand. Neither monotonicity nor integrability of the parametrization's derivative is required. This permits backtracking and unbounded speed.

theorem TauCeti.BoxIntegral.hasIntegral_Henstock_deriv_smul_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a b : ℝ} (hab : a < b) {f : ℝ → E} {θ θ' : ℝ → ℝ} {s : Set ℝ} (hs : s.Countable) (hθ : ContinuousOn θ (Set.Icc a b)) (hdθ : ∀ t ∈ Set.Ioo a b \ s, HasDerivAt θ (θ' t) t) (hf : ContinuousOn f (θ '' Set.Icc a b)) : BoxIntegral.HasIntegral (intervalBox a b hab) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => θ' (x 0) • f (θ (x 0))) BoxIntegral.BoxAdditiveMap.volume (∫ (x : ℝ) in θ a..θ b, f x)

Substitution in the Henstock–Kurzweil integral, for a continuous parametrization differentiable outside a countable exceptional set. The integrand only needs to be continuous on the image of the parametrization.