Derivatives of improper tail integrals

For an integrable function f on (a, ∞), its tail integral t ↦ ∫ s in Ioi t, f s has derivative -f t at each t > a where f is continuous. If f is continuous on the whole ray, the derivative identity also gives a formula for every higher iterated derivative. These results apply to Banach-space-valued integrands and support differential closure arguments for improper integrals.

References

• Mathlib's intervalIntegral.integral_Ioi_sub_Ioi' and intervalIntegral.integral_hasDerivAt_right.

theorem MeasureTheory.IntegrableOn.hasDerivAt_integral_Ioi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a t : ℝ} (hint : IntegrableOn f (Set.Ioi a) volume) (hcont : ContinuousAt f t) (ht : a < t) : HasDerivAt (fun (u : ℝ) => ∫ (s : ℝ) in Set.Ioi u, f s) (-f t) t

At a continuity point strictly inside an integrable ray, the tail integral has derivative equal to the negated integrand.

theorem MeasureTheory.IntegrableOn.deriv_integral_Ioi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a t : ℝ} (hint : IntegrableOn f (Set.Ioi a) volume) (hcont : ContinuousAt f t) (ht : a < t) : deriv (fun (u : ℝ) => ∫ (s : ℝ) in Set.Ioi u, f s) t = -f t

The derivative of an improper tail integral is the negated integrand at each continuity point strictly inside the integrable ray.

theorem MeasureTheory.IntegrableOn.iteratedDeriv_integral_Ioi {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a t : ℝ} (hint : IntegrableOn f (Set.Ioi a) volume) (hcont : ContinuousOn f (Set.Ioi a)) (n : ℕ) (ht : a < t) : iteratedDeriv (n + 1) (fun (u : ℝ) => ∫ (s : ℝ) in Set.Ioi u, f s) t = -iteratedDeriv n f t

For a continuous integrand on an integrable ray, the derivative of order n + 1 of its tail integral is the negated derivative of order n of the integrand at each interior point. The identity concerns total iterated derivatives and does not assume higher smoothness.