Measure-preserving Lipschitz changes of variables in W^{1,p} #
Let Φ : E → E' be a measure-preserving map between finite-dimensional real inner product spaces
carrying additive Haar measures, and let U = Φ⁻¹(V) for open sets U ⊆ E, V ⊆ E'. If Φ is
locally Lipschitz on U with ‖fderiv ℝ Φ x‖ ≤ M there, precomposition with Φ is a bounded
linear operator
TauCeti.W1p.compMeasurePreservingL : W^{1,p}(V) →L[ℝ] W^{1,p}(U),
of norm at most max 1 M. The value of u ∘ Φ is u ∘ Φ and its weak gradient is
x ↦ (fderiv ℝ Φ x)† (∇u (Φ x)), the weak chain rule
TauCeti.HasWeakFDerivOn.comp_measurePreserving read through the Riesz representation. For
p < ∞ and Φ proper (for instance a homeomorphism) the operator maps W^{1,p}_0(V) into
W^{1,p}_0(U): a test function on V composed with Φ is supported in the compact set
Φ⁻¹(tsupport φ) ⊆ U.
Such changes of variables are the local charts of the boundary theory: a shear of a product
flattens the region above the graph of a Lipschitz function onto a half-space, and transports the
half-space trace to that region. Since fderiv ℝ Φ vanishes where Φ is not differentiable, a
K-Lipschitz Φ satisfies the derivative bound with M = K (norm_fderiv_le_of_lipschitz).
Main declarations #
TauCeti.W1p.compMeasurePreservingL: the composition operator.TauCeti.W1p.value_compMeasurePreservingL_ae,TauCeti.W1p.gradient_compMeasurePreservingL_ae: its value and weak gradient.TauCeti.W1p.norm_compMeasurePreservingL_le: the bound‖u ∘ Φ‖ ≤ max 1 M ‖u‖.TauCeti.W1p.compMeasurePreservingL_mem_w1p0Submodule: zero boundary values are preserved.TauCeti.W1p.compMeasurePreservingL_mem_w1p0Submodule_of_contDiff: the same for smooth properΦand every exponent, without mollification.TauCeti.W1p.compAffineIsometryEquivL: precomposition with an affine isometryg, the rigid change of coordinates of a boundary chart. Its weak gradient atxis the inverse of the linear part ofgapplied to∇u (g x), and it does not increase the norm. It preserves and reflects zero boundary values (TauCeti.W1p.compAffineIsometryEquivL_mem_w1p0Submodule_iff).TauCeti.W1p.setIntegral_inner_gradient_compAffineIsometryEquivL: the Dirichlet pairing∫ ⟪∇u, ∇φ⟫ofuagainst a test functionφis invariant under a linear isometric change of coordinates.TauCeti.W1p.setIntegral_inner_gradient_compAffineIsometryEquivL_eq_setIntegral_mul: a weak solution of-Δu = fstays a weak solution, of-Δ(u ∘ e) = f ∘ e, after a linear isometric change of coordinatese.
Precomposition with a measure-preserving Lipschitz map on W^{1,p}. If
U = Φ⁻¹(V) and Φ is locally Lipschitz on U with ‖fderiv ℝ Φ‖ ≤ M there, then
u ↦ u ∘ Φ maps W^{1,p}(V) to W^{1,p}(U), with weak gradient x ↦ (fderiv ℝ Φ x)† (∇u (Φ x))
(TauCeti.W1p.value_compMeasurePreservingL_ae, TauCeti.W1p.gradient_compMeasurePreservingL_ae).
Instances For
The value of u ∘ Φ is the composition of the value of u with Φ.
The chain rule in W^{1,p}: the weak gradient of u ∘ Φ at x is the adjoint of
fderiv ℝ Φ x applied to the weak gradient of u at Φ x.
Precomposition with Φ multiplies the W^{1,p} norm by at most max 1 M.
Precomposition with Φ undoes precomposition with a left inverse Ψ of Φ on U:
(u ∘ Ψ) ∘ Φ = u.
Zero boundary values are preserved. For p < ∞ and a proper map Φ, precomposition
with Φ maps W^{1,p}_0(V) into W^{1,p}_0(U).
Zero boundary values are preserved by smooth proper changes of variables. If Φ is smooth
and proper, precomposition with Φ maps W^{1,p}_0(V) into W^{1,p}_0(U), for every exponent:
the composite φ ∘ Φ of a test function is again a test function, so no mollification is needed
(compare TauCeti.W1p.compMeasurePreservingL_mem_w1p0Submodule, which needs p < ∞).
Affine isometries #
Rigid changes of variables in W^{1,p}. Precomposition with an affine isometry g is a
bounded operator from W^{1,p}(V) to W^{1,p}(U) for U = g⁻¹(V), of norm at most one
(TauCeti.W1p.norm_compAffineIsometryEquivL_le).
Instances For
The value of u ∘ g is the composition of the value of u with g.
The weak gradient of u ∘ g is the gradient of u at g x, pulled back by the inverse of
the linear part of g.
Precomposition with an affine isometry does not increase the W^{1,p} norm.
Rigid changes of coordinates preserve zero Sobolev boundary values.
Precomposition with g.symm undoes precomposition with g: (u ∘ g) ∘ g⁻¹ = u.
Zero boundary values are invariant under rigid changes of coordinates. For
U = g⁻¹(V), the function u ∘ g lies in W^{1,p}_0(U) exactly when u lies in
W^{1,p}_0(V).
The Dirichlet pairing under a linear isometry. For a linear isometry equivalence e and
U = e⁻¹(V), pairing the gradient of u ∘ e with the gradient of a test function φ on U is
the same as pairing the gradient of u with the gradient of the transported test function
φ ∘ e⁻¹ on V.
Poisson's equation under a linear isometry. For a linear isometry equivalence e and
U = e⁻¹(V), if u solves -Δu = f weakly on V, that is ∫_V ⟪∇u, ∇ψ⟫ = ∫_V f ψ for every
test function ψ on V, then u ∘ e solves -Δ(u ∘ e) = f ∘ e weakly on U.