Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul

∀ {f g : ℝ → ℝ} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b →
      ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x

Integration by parts for absolutely continuous functions.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Cited by

1 results in Mathlib

Foundations

Depth 273 from the axioms · uses propext, Classical.choice, Quot.sound