English
A variant stating that if the derivative is integrable and the derivative is bounded in norm, then the integral convergence yields the integrability of f on the tail Ioi(a).
Русский
Если производная интегрируема и нормa её ограничена, то интегрируемость функции на хвосте Ioi(a).
LaTeX
$$$\\text{IntegrableOn}\\ f'\\ Ioi(a)\\to \\text{IntegrableOn}\\ f\\ (Ioi(a)).$$$
Lean4
/-- A special case of `integral_Ioi_of_hasDerivAt_of_tendsto` where we assume that `f` is C^1 with
compact support. -/
theorem _root_.HasCompactSupport.integral_Ioi_deriv_eq (hf : ContDiff ℝ 1 f) (h2f : HasCompactSupport f) (b : ℝ) :
∫ x in Ioi b, deriv f x = -f b :=
by
have := fun x (_ : x ∈ Ioi b) ↦ hf.differentiable le_rfl x |>.hasDerivAt
rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]
· refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn
rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto
