English
Under assumptions with a real-valued function on Iic a, and derivative conditions, an improper integral identity holds between Iic and other intervals.
Русский
При предположениях на функцию на Iic a и условия на производные выполняется идентичность интегралов между Iic и другими интервалами.
LaTeX
$$$$ \int_{x \le a} f'(x) dx = f(a) - \lim_{x\to -\infty} f(x). $$$$
Lean4
/-- **Integration by parts on (a, ∞).**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`. -/
theorem integral_Ioi_mul_deriv_eq_deriv_mul (hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x)
(hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x) (huv' : IntegrableOn (u * v') (Ioi a))
(hu'v : IntegrableOn (u' * v) (Ioi a)) (h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a'))
(h_infty : Tendsto (u * v) atTop (𝓝 b')) :
∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x :=
by
rw [Pi.mul_def] at huv' hu'v
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
simpa only [add_comm] using integral_Ioi_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty
