Integration by parts and by substitution #
We derive additional integration techniques from FTC-2:
intervalIntegral.integral_mul_deriv_eq_deriv_mul- integration by partsintervalIntegral.integral_comp_mul_deriv''- integration by substitution
Versions of the change of variables formula for monotone and antitone functions, but with much
weaker assumptions on the integrands and not restricted to intervals,
can be found in Mathlib/MeasureTheory/Function/JacobianOneDim.lean
Tags #
integration by parts, change of variables in integrals
The integral of the derivative of a product of two maps.
For improper integrals, see MeasureTheory.integral_deriv_mul_eq_sub,
MeasureTheory.integral_Ioi_deriv_mul_eq_sub, and MeasureTheory.integral_Iic_deriv_mul_eq_sub.
The integral of the derivative of a product of two maps.
Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a
two-sided derivative in the interior of the interval.
The integral of the derivative of a product of two maps.
Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a
one-sided derivative at the endpoints.
Special case of integral_deriv_mul_eq_sub_of_hasDeriv_right where the functions have a
derivative at the endpoints.
Integration by parts. For improper integrals, see
MeasureTheory.integral_mul_deriv_eq_deriv_mul,
MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul,
and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.
Integration by parts. Special case of integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right
where the functions have a two-sided derivative in the interior of the interval.
Integration by parts. Special case of
intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right
where the functions have a one-sided derivative at the endpoints.
Integration by parts. Special case of
intervalIntegrable.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right
where the functions have a derivative also at the endpoints.
For improper integrals, see
MeasureTheory.integral_mul_deriv_eq_deriv_mul,
MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul,
and MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul.
The integral of the derivative of a scalar multiplication.
Integration by parts (vector-valued).
Integration by parts (vector-valued).
Special case of integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right
where the functions have a two-sided derivative in the interior of the interval.
Integration by parts (vector-valued). Special case of
intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right
where the functions have a one-sided derivative at the endpoints.
Integration by parts (vector-valued). Special case of
intervalIntegrable.integral_smul_deriv_eq_deriv_smul_of_hasDeriv_right
where the functions have a derivative also at the endpoints.
Integration by substitution / Change of variables #
Change of variables, general form. If f is continuous on [a, b] and has
right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on
f '' [a, b], and f' x • (g ∘ f) x is integrable on [a, b],
then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Alias of intervalIntegral.integral_deriv_smul_comp'''.
Change of variables, general form. If f is continuous on [a, b] and has
right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on
f '' [a, b], and f' x • (g ∘ f) x is integrable on [a, b],
then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Change of variables for continuous integrands. If f is continuous on [a, b] and has
continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can
substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Alias of intervalIntegral.integral_deriv_smul_comp''.
Change of variables for continuous integrands. If f is continuous on [a, b] and has
continuous right-derivative f' in (a, b), and g is continuous on f '' [a, b] then we can
substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Change of variables. If f has continuous derivative f' on [a, b],
and g is continuous on f '' [a, b], then we can substitute u = f x to get
∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
Compared to intervalIntegral.integral_deriv_smul_comp we only require that g is continuous on
f '' [a, b].
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Alias of intervalIntegral.integral_deriv_smul_comp'.
Change of variables. If f has continuous derivative f' on [a, b],
and g is continuous on f '' [a, b], then we can substitute u = f x to get
∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
Compared to intervalIntegral.integral_deriv_smul_comp we only require that g is continuous on
f '' [a, b].
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Change of variables, most common version. If f has continuous derivative f' on [a, b],
and g is continuous, then we can substitute u = f x to get
∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
Alias of intervalIntegral.integral_deriv_smul_comp.
Change of variables, most common version. If f has continuous derivative f' on [a, b],
and g is continuous, then we can substitute u = f x to get
∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
If the function f is monotone or antitone, see also integral_deriv_smul_comp_of_deriv_nonneg
and integral_deriv_smul_comp_of_deriv_nonpos dropping all assumptions on g.
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, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
Change of variables for antitone functions.
If f is continuous on [a, b] and has a nonpositive derivative f' in (a, b),
then we can substitute u = f x to get ∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u.
Change of variables, general form for scalar functions. If f is continuous on [a, b] and has
continuous right-derivative f' in (a, b), g is continuous on f '' (a, b) and integrable on
f '' [a, b], and (g ∘ f) x * f' x is integrable on [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.
Change of variables for continuous integrands. If f is continuous on [a, b] and has
continuous right-derivative f' in (a, b), and g is continuous on f '' [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.
Change of variables. If f has continuous derivative f' on [a, b],
and g is continuous on f '' [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.
Compared to intervalIntegral.integral_comp_mul_deriv we only require that g is continuous on
f '' [a, b].
Change of variables, most common version. If f has continuous derivative f' on [a, b],
and g is continuous, 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.
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.
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.