Theorems · Theorem · real analysis

intervalIntegral.integral_comp_mul_deriv_of_deriv_nonpos

∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), f' x ≤ 0) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u

Change of variables for monotone functions. If f is continuous on [a, b] and has a nonnegative derivative f' in (a, b), then we can substitute u = f x to get ∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Cited by

1 results in Mathlib

Foundations

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