Theorems · Theorem · measure theory

MeasureTheory.integral_comp_mul_deriv_Ioi

∀ {f f' g : ℝ → ℝ} {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 => (g ∘ f) x * f' x) (Set.Ici a) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Set.Ioi (f a), g u

Change-of-variables formula for Ioi integrals of scalar-valued functions

Defined in: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Cited by: 1 results in Mathlib
Foundations: Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Realstatement and proof · cited by 25,697
Set.imagestatement and proof · cited by 5,609
Filter.Tendstostatement and proof · cited by 3,814
Filter.atTopstatement and proof · cited by 2,405
mul_commproof · cited by 2,262
MeasureTheory.integralstatement and proof · cited by 1,779
MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
Set.Ioistatement and proof · cited by 1,463
ContinuousOnstatement and proof · cited by 1,411
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
Set.Icistatement and proof · cited by 1,070

Cited by1

Results whose statement or proof uses this declaration.

Real.integral_rpowIntegrand₀₁_eq_rpow_mul_constproof · cited by 1