The Lᵖ translation estimate on W^{1,p}_0 #
This file transports the translation estimate to Sobolev functions: for 1 ≤ p < ∞ and a
vector h,
‖u(· + h) - u‖_p ≤ ‖h‖ ‖∇u‖_p.
It is the quantitative form of the continuity of translation in Lᵖ, with a modulus that is
linear in ‖h‖ and controlled by one Sobolev seminorm. The ambient space is any
finite-dimensional real inner product space E carrying an arbitrary additive Haar measure mu,
not just ℝⁿ with Lebesgue measure; ℝⁿ is used informally below for the whole-space case
Ω = ⊤. Together with the extension of a W^{1,p}_0(Ω) function by zero, it supplies the
uniform smallness of translations hypothesis of the Fréchet--Kolmogorov compactness criterion,
and so is the analytic input for Rellich--Kondrachov, Lane A.6 of
TauCetiRoadmap/PDE/README.md.
The estimate on W^{1,p}_0(ℝⁿ) #
TauCeti.W1p.eLpNorm_value_comp_add_sub_value_le_mul_enorm_gradient transports the C¹ estimate
from TauCeti.MeasureTheory.Function.Lp.Translation to the Sobolev space by density. The set of
jets satisfying it is closed — the translation increment is a continuous function of the Lᵖ
class, being the difference of the identity and the isometry induced by a measure-preserving map
— and it contains every test-function jet, so
TauCeti.w1p0Submodule_subset_of_isClosed gives it on all of W^{1,p}_0(ℝⁿ). Note that the
whole space is where a translation estimate can be stated without further data: translating a
function defined on a proper open Ω moves it off Ω, so the general case is this statement
composed with an extension of W^{1,p}_0(Ω) by zero.
The theorem assumes membership in W^{1,p}_0(ℝⁿ), the closure of the test functions, because
test-function density is the available route to the whole-space estimate. Since Ω = ⊤ has no
boundary, this is not an additional boundary condition. For a proper Ω, however, transferring
the estimate by zero extension does require W^{1,p}_0(Ω): the zero-extension of a general
Sobolev function need not be weakly differentiable across ∂Ω. A local form on W^{1,p}(Ω)
survives on compactly contained subsets for translations smaller than their distance to the
boundary.
Translation after extension by zero #
For an arbitrary open domain Ω, the translation estimate is applied after extending by zero to
the whole space. TauCeti.W1p0.eLpNorm_value_extendByZeroL_comp_add_sub_le_mul_enorm_gradient
records the result directly in terms of the original gradient:
‖\tilde{u}(· + h) - \tilde{u}‖_p ≤ ‖h‖ ‖∇u‖_p,
where \tilde{u} is the zero extension of u. The zero extension vanishes almost everywhere
off Ω, as recorded by TauCeti.W1p0.value_extendByZeroL_ae_eq_zero_compl, so its support is
contained in Ω up to a null set. When Ω is bounded, this containment and the translation
estimate give the fixed-bounded-support and translation inputs for Fréchet--Kolmogorov.
Main declarations #
TauCeti.W1p.eLpNorm_value_comp_add_sub_value_le_mul_enorm_gradient: the translation estimate onW^{1,p}_0(ℝⁿ).TauCeti.W1p0.eLpNorm_value_extendByZeroL_comp_add_sub_le_mul_enorm_gradient: the translation estimate for the zero extension of a function inW^{1,p}_0(Ω).TauCeti.W1p0.exists_pos_forall_eLpNorm_value_extendByZeroL_comp_add_sub_le_of_gradient_le: zero extensions of a gradient-bounded family have uniformly small translation increments.TauCeti.W1p0.exists_pos_forall_eLpNorm_value_extendByZeroL_comp_add_sub_le_of_norm_le: zero extensions of a norm-bounded family have uniformly small translation increments.TauCeti.Sobolev1JetLp.value_translateLp,TauCeti.Sobolev1JetLp.gradient_translateLp: translating a whole-space jet translates its value and gradient components.TauCeti.Sobolev1JetLp.translateLp_mem_w1pSubmodule: translation preservesW^{1,p}(ℝⁿ), since on the whole space the weak-derivative identities are translation invariant.
References #
Lane A.6 of TauCetiRoadmap/PDE/README.md; H. Brezis, Functional Analysis, Sobolev Spaces and
Partial Differential Equations, Proposition 9.3, for the estimate, and Theorem 4.26 for the
Fréchet--Kolmogorov criterion it feeds; L. C. Evans, Partial Differential Equations,
Chapter 5, for the difference-quotient form of the same bound.
The translation estimate on W^{1,p}_0(ℝⁿ): for 1 ≤ p < ∞, every u in the closure of
the test functions satisfies
‖u(· + h) - u‖_p ≤ ‖h‖ ‖∇u‖_p.
The estimate for a single test function comes from
ContDiff.eLpNorm_comp_add_sub_le_mul_eLpNorm_fderiv; the set of jets obeying it is closed, so
TauCeti.w1p0Submodule_subset_of_isClosed passes it to the closure. Composing with a
zero-extension operator turns this into the corresponding estimate on W^{1,p}_0(Ω) for an
arbitrary open Ω, which is the form the Fréchet--Kolmogorov compactness criterion consumes in
the proof of Rellich--Kondrachov.
Translation after extension by zero #
The translation estimate on W^{1,p}_0(Ω) for an arbitrary open Ω: for 1 ≤ p < ∞,
the extension by zero of u ∈ W^{1,p}_0(Ω) satisfies
‖u(· + h) - u‖_p ≤ ‖h‖ ‖∇u‖_p
on the whole space. This is the whole-space estimate
TauCeti.W1p.eLpNorm_value_comp_add_sub_value_le_mul_enorm_gradient composed with the
zero-extension operator TauCeti.W1p0.extendByZeroL. Extension by zero is an isometry on the
gradient component, so the right-hand side is the gradient seminorm of u on Ω itself and
nothing is lost in the transfer. This is the form the Fréchet--Kolmogorov criterion consumes in
the proof of Rellich--Kondrachov.
Uniform smallness of translation increments for a gradient-bounded Sobolev family. If
every u ∈ S ⊆ W^{1,p}_0(Ω) has gradient norm at most C, then for every ε > 0 there is a
common δ > 0 such that every zero extension \tilde{u} satisfies
‖\tilde{u}(· + h) - \tilde{u}‖_p ≤ ε whenever ‖h‖ < δ.
When Ω is bounded, TauCeti.W1p0.value_extendByZeroL_ae_eq_zero_compl also supplies fixed
bounded support for the family.
Uniform smallness of translation increments for a norm-bounded Sobolev family. This is
the graph-norm-bounded corollary of
TauCeti.W1p0.exists_pos_forall_eLpNorm_value_extendByZeroL_comp_add_sub_le_of_gradient_le.
Translation preserves W^{1,p}(ℝⁿ) #
The whole-space restriction of an additive Haar measure is the measure itself.
The value component of a translated whole-space jet is the translate of its value component.
The gradient component of a translated whole-space jet is the translate of its gradient component.
Translation preserves W^{1,p}(ℝⁿ). On the whole space the weak-derivative identities
are invariant under translation: testing the translated jet against φ is testing the original
jet against the translate of φ.