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.

We also give more specific versions of these theorems for monotone and antitone functions: this makes it possible to drop the injectivity assumption of the general theorems, as the derivative is zero on the set of non-injectivity, which means that it can be discarded.

See also Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean 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 MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf : MonotoneOn f s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : ∃ (a : Set ℝ) (b : Set ℝ) (c : Set ℝ), a ∪ (b ∪ c) = s ∧ MeasurableSet a ∧ MeasurableSet b ∧ MeasurableSet c ∧ Disjoint a (b ∪ c) ∧ Disjoint b c ∧ a.Countable ∧ (f '' b).Countable ∧ (∀ x ∈ b, f' x = 0) ∧ (∀ x ∈ c, 0 ≤ f' x) ∧ Set.InjOn f c

Technical structure theorem for monotone differentiable functions.

If a function f is monotone on a measurable set and has a derivative f', one can decompose the set as a disjoint union a ∪ b ∪ c of measurable sets where a is countable (the points which are isolated on the left or on the right, where f' is not well controlled), f is locally constant on b and f' = 0 there (the preimages of the countably many points with several preimages), and f is injective on c with nonnegative derivative (the other points).

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

theorem MeasureTheory.lintegral_deriv_eq_volume_image_of_monotoneOn {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : MonotoneOn f s) : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) = volume (f '' s)

Change of variable formula for differentiable functions, set version: if a real function f is monotone and differentiable on a measurable set s, then the measure of f '' s is given by the integral of f' x on s . Note that the measurability of f '' s is given by MeasurableSet.image_of_monotoneOn.

theorem MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn {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 : MonotoneOn 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: if a real function f is monotone 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_deriv_smul_of_monotoneOn {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 : MonotoneOn 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: if a real function f is monotone 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 MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) (u : ℝ → ENNReal) : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)

theorem MeasureTheory.lintegral_deriv_eq_volume_image_of_antitoneOn {s : Set ℝ} {f f' : ℝ → ℝ} (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : AntitoneOn f s) : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) = volume (f '' s)

Change of variable formula for differentiable functions, set version: if a real function f is antitone and differentiable on a measurable set s, then the measure of f '' s is given by the integral of -f' x on s . Note that the measurability of f '' s is given by MeasurableSet.image_of_antitoneOn.

theorem MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn {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 : AntitoneOn 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: if a real function f is antitone 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_deriv_smul_of_antitone {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 : AntitoneOn 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: if a real function f is antitone 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))