The weak chain rule for measure-preserving Lipschitz changes of variables

Let Φ : E → E' be a measure-preserving map between finite-dimensional real normed spaces carrying additive Haar measures, locally Lipschitz on an open set U ⊆ E, with Φ '' U ⊆ V for an open set V ⊆ E'. If u has weak derivative D on V, then u ∘ Φ has weak derivative

x ↦ D (Φ x) ∘L fderiv ℝ Φ x

on U: the classical chain rule survives the passage to weak derivatives. By Rademacher's theorem Φ is differentiable almost everywhere on U, which is all the formula needs. No global bound on the derivative of Φ and no integrability of u beyond local integrability is needed, because weak derivatives are detected on relatively compact subdomains.

The typical change of variables of this kind is a shear (t, y) ↦ (t - φ y, y) of a product, which flattens the region above the graph of a Lipschitz function φ onto a half-space; it is measure-preserving by Fubini's theorem.

The argument

Fix an open W whose closure is compact and contained in U. The image K = Φ '' closure W is compact in V, so some open thickening O of K still lies in V, and u, D are integrable on O. Mollify the zero extensions of u and D from O by normalized bumps of radius less than the thickening. The mollified u is smooth with compact support, hence Lipschitz, and near K its derivative is the mollified D (TauCeti.HasWeakFDerivOn.hasFDerivAt_indicator_convolution_normed). Its composition with Φ is therefore Lipschitz on W, with derivative given by the classical chain rule wherever Φ is differentiable, so it is weakly differentiable (LocallyLipschitzOn.hasWeakFDerivOn). Since Φ is measure-preserving, the L¹(W) distances to u ∘ Φ and to the candidate derivative are bounded by the L¹ distances of the mollifications to the zero extensions, the latter multiplied by a Lipschitz constant of Φ on closure W, and these tend to zero (TauCeti.tendsto_eLpNorm_normed_convolution_sub). Weak derivatives pass to such limits (TauCeti.hasWeakFDerivOn_of_tendsto_lintegral_enorm_sub).

Main declarations

• TauCeti.HasWeakFDerivOn.comp_measurePreserving: the weak chain rule.
• TauCeti.HasWeakFDerivOn.comp_continuousLinearEquiv, ContinuousLinearEquiv.hasWeakFDerivOn_comp_iff: the case of a measure-preserving continuous linear equivalence, such as a linear isometry between inner product spaces.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.3 (smooth approximation).
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 9.6.
• W. P. Ziemer, Weakly Differentiable Functions, §2.2 (bi-Lipschitz changes of variables).

theorem TauCeti.HasWeakFDerivOn.comp_measurePreserving {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure E'} [BorelSpace E] [μ.IsAddHaarMeasure] [BorelSpace E'] [ν.IsAddHaarMeasure] {U : TopologicalSpace.Opens E} {V : TopologicalSpace.Opens E'} {u : E' → F} {D : E' → E' →L[ℝ] F} {Φ : E → E'} (h : HasWeakFDerivOn ν V u D) (hΦ : MeasureTheory.MeasurePreserving Φ μ ν) (hΦl : LocallyLipschitzOn (↑U) Φ) (hUV : Set.MapsTo Φ ↑U ↑V) : HasWeakFDerivOn μ U (u ∘ Φ) fun (x : E) => D (Φ x) ∘SL fderiv ℝ Φ x

The weak chain rule. If u has weak derivative D on the open set V, and Φ is a measure-preserving map, locally Lipschitz on the open set U and mapping U into V, then u ∘ Φ has weak derivative x ↦ D (Φ x) ∘L fderiv ℝ Φ x on U.

theorem TauCeti.HasWeakFDerivOn.comp_continuousLinearEquiv {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure E'} [BorelSpace E] [μ.IsAddHaarMeasure] [BorelSpace E'] [ν.IsAddHaarMeasure] {U : TopologicalSpace.Opens E} {V : TopologicalSpace.Opens E'} {u : E' → F} {D : E' → E' →L[ℝ] F} (h : HasWeakFDerivOn ν V u D) (e : E ≃L[ℝ] E') (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) (hUV : Set.MapsTo ⇑e ↑U ↑V) : HasWeakFDerivOn μ U (u ∘ ⇑e) fun (x : E) => D (e x) ∘SL ↑e

The weak chain rule for linear changes of variables. If u has weak derivative D on the open set V, and the continuous linear equivalence e carries μ to ν and maps U into V, then u ∘ e has weak derivative x ↦ D (e x) ∘L e on U. Linear isometries between finite-dimensional real inner product spaces carry volume to volume (LinearIsometryEquiv.measurePreserving).

theorem ContinuousLinearEquiv.hasWeakFDerivOn_comp_iff {E : Type u_1} {E' : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [MeasurableSpace E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure E'} [BorelSpace E] [μ.IsAddHaarMeasure] [BorelSpace E'] [ν.IsAddHaarMeasure] {U : TopologicalSpace.Opens E} {V : TopologicalSpace.Opens E'} {u : E' → F} {D : E' → E' →L[ℝ] F} (e : E ≃L[ℝ] E') (he : MeasureTheory.MeasurePreserving (⇑e) μ ν) (hUV : ↑U = ⇑e ⁻¹' ↑V) : (TauCeti.HasWeakFDerivOn μ U (u ∘ ⇑e) fun (x : E) => D (e x) ∘SL ↑e) ↔ TauCeti.HasWeakFDerivOn ν V u D

Weak derivatives through a linear change of variables. If the continuous linear equivalence e carries μ to ν and U = e ⁻¹' V, then u ∘ e has weak derivative x ↦ D (e x) ∘L e on U exactly when u has weak derivative D on V.