Scalar fundamental theorem on a finite halfspace slice

Integration of a compactly supported scalar derivative over the interval cut out by finitely many affine inequalities, with the endpoints written as the signed sum of genuine transverse constraint values.

theorem LiebThirring.integral_derivative_finite_halfspaces {ι : Type u_1} [Fintype ι] (a b : ι → ℝ) (hregular : ∀ (t : ℝ) (i j : ι), i ≠ j → (∀ (p : ι), t * a p ≤ b p) → t * a i = b i → t * a j = b j → False) (g g' : ℝ → ℝ) (hg : ∀ (t : ℝ), HasDerivAt g (g' t) t) (hg' : Continuous g') (hgc : HasCompactSupport g) (hg'c : HasCompactSupport g') : ∫ (t : ℝ) in {t : ℝ | ∀ (i : ι), t * a i < b i}, g' t = (∑ i : ι, if 0 < a i then halfspaceFaceValue a b g i else 0) - ∑ i : ι, if a i < 0 then halfspaceFaceValue a b g i else 0