Theorems · Theorem · measure theory

MeasureTheory.integral_deriv_smul_comp_Ioi

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ},
  ContinuousOn f (Set.Ici a) →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        ContinuousOn g (f '' Set.Ioi a) →
          MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
            MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.Ici a) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Set.Ioi (f a), g u

Change-of-variables formula for Ioi integrals of vector-valued functions, proved by taking limits from the result for finite intervals.

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace