Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub

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

The integral of the derivative of a product of two absolutely continuous functions.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Cited by

1 results in Mathlib

Foundations

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