Change of variables: pushforward bounds, Lᵖ bounds and affine invariance of set integrals #
Let f be injective and differentiable on a null-measurable subset s of a finite-dimensional real
normed space with an additive Haar measure μ. Mathlib's change of variables formula
MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar says that f pushes the measure
|det f'| μ on s forward to μ on f '' s. If the Jacobian is bounded below, c ≤ |det f'|
on s with c > 0, then f pushes μ on s forward to at most c⁻¹ μ on f '' s
(MeasureTheory.map_restrict_le_smul_restrict_image).
For f differentiable on an open set s and mapping it into t, the same bound holds with the
Fréchet derivative fderiv ℝ f as Jacobian and μ on t in place of μ on f '' s
(MeasureTheory.map_restrict_le_smul_restrict_of_differentiableOn).
Such a pushforward bound μ.map f ≤ C • ν gives the eLpNorm estimate for precomposition with
f (MeasureTheory.eLpNorm_comp_le_of_map_le_smul). For a change of variables no upper bound on
the Jacobian is needed, but a Jacobian that may vanish gives no such bound. On a measurable set s
inside an open set where f is differentiable, with f injective on s and given constants
c ≤ |det Df| and ‖Df‖ ≤ L on s, this bounds the Lᵖ(s) norms of u ∘ f and of the
transformed derivative x ↦ D (f x) ∘ Df x by those of u and D on f '' s
(MeasureTheory.eLpNorm_comp_restrict_le, MeasureTheory.eLpNorm_comp_fderiv_restrict_le).
Such constants exist on every compact set on which a C¹ map has invertible derivative
(MeasureTheory.exists_det_bounds_of_isCompact), so precomposition with a map that is C¹,
injective and with invertible derivative on an open set preserves local integrability
(MeasureTheory.LocallyIntegrableOn.comp_contDiffOn_diffeo).
A continuous affine map T carrying a measurable set s of finite measure onto itself preserves
integrals over s. When s is not null, the linear part of T has determinant ±1, because the
image of s has |det| times the measure of s, so the change of variables formula has no
Jacobian factor
(ContinuousAffineMap.setIntegral_comp_of_image_eq). This is how a symmetry of a polytope, such as
a permutation of the vertices of a simplex, acts on integrals over it.
Main declarations #
MeasureTheory.map_restrict_le_smul_restrict_image: the pushforward ofμonsis at mostc⁻¹ μonf '' s.MeasureTheory.map_restrict_le_smul_restrict_of_differentiableOn: the same forfdifferentiable on an open setsand mapping it intot, withμontas the target.MeasureTheory.exists_det_bounds_of_isCompact: Jacobian and derivative bounds on a compact set.MeasureTheory.eLpNorm_comp_restrict_le,MeasureTheory.eLpNorm_comp_fderiv_restrict_le: theLᵖbounds for precomposition on a measurable set, given such constants.MeasureTheory.MemLp.comp_restrict_of_isCompact,MeasureTheory.MemLp.comp_fderiv_restrict_of_isCompact: precomposition on a compact set.MeasureTheory.LocallyIntegrableOn.comp_contDiffOn_diffeo,MeasureTheory.LocallyIntegrableOn.comp_fderiv_contDiffOn_diffeo: local integrability is preserved.ContinuousAffineMap.setIntegral_comp_of_image_eq: integrals oversare invariant under a continuous affine map carryingsonto itself, whenshas finite measure.
Pushforward bound from a Jacobian lower bound. If f is injective and differentiable on
a null-measurable set s, and c ≤ |det f'| on s with c > 0, then f pushes μ restricted to
s forward to at most c⁻¹ times μ restricted to f '' s.
Pushforward bound on a subset of an open set of differentiability. If f is
differentiable on an open set Ω, injective on a measurable set s ⊆ Ω, and
c ≤ |det (fderiv ℝ f x)| on s with c > 0, then f pushes μ restricted to s forward to
at most c⁻¹ times μ restricted to f '' s.
Pushforward bound for a map differentiable on an open set. If f is injective and
differentiable on an open set s, maps s into t, and c ≤ |det (fderiv ℝ f x)| on s with
c > 0, then f pushes μ restricted to s forward to at most c⁻¹ times μ restricted to
t.
Jacobian bounds on compact sets and Lᵖ bounds for precomposition #
Jacobian bounds on a compact set. If f is C¹ on an open set Ω and its derivative is
invertible on a compact set K ⊆ Ω, then on K the Jacobian is bounded below by a positive
constant and the derivative is bounded.
Lᵖ bound for precomposition on a measurable set. Under the hypotheses of
MeasureTheory.map_restrict_le_smul_restrict_image_of_differentiableOn,
‖u ∘ f‖_{Lᵖ(s)} ≤ c^(-1/p) ‖u‖_{Lᵖ(f s)}.
Precomposition with f maps Lᵖ(f s) into Lᵖ(s) under the hypotheses of
MeasureTheory.eLpNorm_comp_restrict_le.
Lᵖ bound for the transformed derivative on a measurable set. If moreover
‖fderiv ℝ f‖ ≤ L on s, then for D almost everywhere strongly measurable on f s,
‖D ∘ f ∘ Df‖_{Lᵖ(s)} ≤ L c^(-1/p) ‖D‖_{Lᵖ(f s)}.
Precomposition with f followed by composition with fderiv ℝ f maps Lᵖ(f s) into
Lᵖ(s) under the hypotheses of MeasureTheory.eLpNorm_comp_fderiv_restrict_le.
Precomposition on a compact set. If f is C¹ on an open set Ω, and injective with
invertible derivative on a compact set K ⊆ Ω, then precomposition with f maps Lᵖ(f K) into
Lᵖ(K).
The transformed derivative on a compact set. Under the hypotheses of
MeasureTheory.MemLp.comp_restrict_of_isCompact, x ↦ D (f x) ∘ fderiv ℝ f x is in Lᵖ(K)
whenever D is in Lᵖ(f K).
Local integrability is preserved by precomposition with a map that is C¹, injective and
with invertible derivative on an open set U, mapping U into V.
The transformed derivative x ↦ D (f x) ∘ fderiv ℝ f x is locally integrable on U whenever
D is locally integrable on V, under the hypotheses of
MeasureTheory.LocallyIntegrableOn.comp_contDiffOn_diffeo.
Integrals over a set are invariant under an affine self-map of it. If a continuous affine
map T carries a measurable set s of finite measure onto itself, then
∫ x in s, g (T x) ∂μ = ∫ x in s, g x ∂μ for every g.