Change of variable formulas for integrals in dimension 1

We record in this file versions of the general change of variables formula in integrals for functions from R to ℝ. This makes it possible to replace the determinant of the Fréchet derivative with the one-dimensional derivative.

See also Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts for versions of the change of variables formula in dimension 1 for non-monotone functions, formulated with the interval integral and with stronger requirements on the integrand.

theorem MeasureTheory.lintegral_image_eq_lintegral_abs_deriv_mul {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : ℝ → ENNReal) : ∫⁻ (x : ℝ) in f '' s, g x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal |f' x| * g (f x)

Integrability in the change of variable formula for differentiable functions (one-variable version): if a function f is injective and differentiable on a measurable set s ⊆ ℝ, then the Lebesgue integral of a function g : ℝ → ℝ≥0∞ on f '' s coincides with the Lebesgue integral of |(f' x)| * g ∘ f on s.

theorem MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : ℝ → F) : IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun (x : ℝ) => |f' x| • g (f x)) s volume

Integrability in the change of variable formula for differentiable functions (one-variable version): if a function f is injective and differentiable on a measurable set s ⊆ ℝ, then a function g : ℝ → F is integrable on f '' s if and only if |(f' x)| • g ∘ f is integrable on s.

theorem MeasureTheory.integral_image_eq_integral_abs_deriv_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : Set.InjOn f s) (g : ℝ → F) : ∫ (x : ℝ) in f '' s, g x = ∫ (x : ℝ) in s, |f' x| • g (f x)

Change of variable formula for differentiable functions (one-variable version): if a function f is injective and differentiable on a measurable set s ⊆ ℝ, then the Bochner integral of a function g : ℝ → F on f '' s coincides with the integral of |(f' x)| • g ∘ f on s.

theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s) {g : ℝ → ℝ} (hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x) (hf_int : MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume) {f' : ℝ → ℝ} (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : (MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul (f : ℝ ≃ᵐ ℝ) {s : Set ℝ} (hs : MeasurableSet s) {g : ℝ → ℝ} (hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x) (hf_int : MeasureTheory.IntegrableOn g (⇑f '' s) MeasureTheory.volume) {f' : ℝ → ℝ} (hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x) : (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

theorem MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s) {f' : ℝ → ℝ} (hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x) {g : ℝ → ℝ} (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) : (MeasureTheory.Measure.comap f (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

theorem MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' (f : ℝ ≃ᵐ ℝ) {s : Set ℝ} (hs : MeasurableSet s) {f' : ℝ → ℝ} (hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) {g : ℝ → ℝ} (hg : 0 ≤ᵐ[MeasureTheory.volume] g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) : (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))