Integrating derivatives with countably many exceptional points

A continuous, compactly supported map whose derivative exists outside a countable set has zero integral of each directional derivative (trivially so when that derivative is not integrable, as the integral is then zero by convention). The candidate derivative may take arbitrary values at the exceptional points. This permits integration by parts across isolated singularities without assuming differentiability there.

The proof uses Mathlib's MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable' on a box containing the support, followed by the uniqueness of Haar measure and a linear change of coordinates.

theorem TauCeti.integral_apply_eq_zero_of_hasFDerivAt_off_countable {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → F} {D : E → E →L[ℝ] F} {s : Set E} (hs : s.Countable) (hf : Continuous f) (hfc : HasCompactSupport f) (hd : ∀ x ∉ s, HasFDerivAt f (D x) x) (v : E) : ∫ (x : E), (D x) v ∂μ = 0

The integral of a directional derivative of a continuous compactly supported map is zero, even if the derivative fails to exist on a countable set. The integral of a non-integrable function is zero by convention, so no integrability hypothesis is needed.