Theorems · Theorem · real analysis

intervalIntegral.integral_deriv_smul_deriv_comp

∀ {a b : ℝ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g g' : ℝ → E}
  [CompleteSpace E],
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivAt g (g' (f x)) (f x)) →
      ContinuousOn f' (Set.uIcc a b) → Continuous g' → ∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace