Theorems · Theorem · real analysis

intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right

∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

The integral of the derivative of a product of two maps. For improper integrals, see MeasureTheory.integral_deriv_mul_eq_sub, MeasureTheory.integral_Ioi_deriv_mul_eq_sub, and MeasureTheory.integral_Iic_deriv_mul_eq_sub.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRingNormedAlgebraCompleteSpace