The Lᵖ translation estimate #
This file develops translation of Lᵖ functions by a vector of an additive group carrying a
right-invariant measure, and the quantitative translation estimate for C¹ functions on a real
normed space:
‖u(· + h) - u‖_p ≤ ‖h‖ ‖Du‖_p.
Translation of Lᵖ classes is a linear isometric equivalence, it is an action of the additive
group of vectors, and for p < ∞ it is strongly continuous; consequently the translation
increments of any Lᵖ function tend to zero. The translation estimate is the quantitative form of
this continuity for a C¹ function, and needs no integrability of the function itself.
Main declarations #
MeasureTheory.Lp.continuous_compMeasurePreserving_add_right: strong continuity of translation ofLᵖclasses forp < ∞.MeasureTheory.Measure.translateLp: translation by a vector as a linear isometric equivalence ofLᵖ.MeasureTheory.Measure.coeFn_translateLp,MeasureTheory.MemLp.coeFn_translateLp_toLp: translation is almost everywhere precomposition by addition.MeasureTheory.Measure.compLpL_translateLp: translation commutes with postcomposition by a continuous linear map.MeasureTheory.Measure.translateLp_zero,MeasureTheory.Measure.translateLp_symm,MeasureTheory.Measure.translateLp_add: translation is an action of the additive group of vectors.MeasureTheory.Measure.continuous_translateLp: strong continuity oftranslateLpforp < ∞.MeasureTheory.Measure.enorm_translateLp_sub: identifies the norm of anLᵖtranslation increment with its pointwiseeLpNorm.MeasureTheory.MemLp.comp_add_right_restrict_of_mapsTo: translation preservesLᵖon a smaller domain whose translate stays in the original domain.MeasureTheory.MemLp.tendsto_eLpNorm_comp_add_sub: translation increments of anLᵖfunction tend to zero.ContDiff.setLIntegral_enorm_comp_add_sub_rpow_le,ContDiff.eLpNorm_comp_add_sub_le_eLpNorm_fderiv_apply: the local translation estimate, bounding the increment on a setKby the directional derivative on a set containing the segments[x, x + h],x ∈ K.ContDiff.lintegral_enorm_comp_add_sub_rpow_le,ContDiff.eLpNorm_comp_add_sub_le_mul_eLpNorm_fderiv: the global translation estimate.ContDiff.tendsto_eLpNorm_comp_add_sub: continuity of translation inLᵖfor aC¹function withLᵖderivative.
References #
H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Proposition 9.3; L. C. Evans, Partial Differential Equations, Chapter 5.
Translation of a fixed Lᵖ class depends continuously on the translation vector when
p < ∞.
Translation by h on Lᵖ, as a linear isometric equivalence: almost everywhere it sends f
to f (· + h), and its inverse is translation by -h.
Equations
- mu.translateLp p h = MeasureTheory.Lp.compMeasurePreservingₗᵢEquiv ℝ ⋯ ⋯ ⋯
Instances For
Translation by h is almost everywhere precomposition by addition of h.
Translation commutes with postcomposition by a continuous linear map.
Translating by h₁ + h₂ is translating by h₁ and then by h₂.
Translation by zero is the identity on Lᵖ.
The inverse of translation by h is translation by -h.
Translation of a fixed Lᵖ class depends continuously on the translation vector when
p < ∞.
The Lᵖ extended norm of a translation increment is its pointwise eLpNorm.
The translate of the Lᵖ class of f by h is almost everywhere f (· + h).
An Lᵖ function remains Lᵖ after translation on any set whose translate lies in the
original domain. This is the restricted-domain counterpart of precomposition by
MeasureTheory.Measure.translateLp.
Translation increments of an Lᵖ function tend to zero as the translation tends to zero.
The powered segment estimate in the direction of the increment. For a C¹ function and
r ≥ 1, the r-th power of ‖u(x + h) - u(x)‖ is bounded by the integral along [x, x + h]
of the r-th power of the directional derivative Du · h.
The local translation estimate in ∫⁻ form: for a C¹ function and 1 ≤ r, if every
segment [x, x + h] starting in K lies in the measurable set T, then
∫_K ‖u(x + h) - u(x)‖ ^ r dx ≤ ∫_T ‖Du(x) h‖ ^ r dx.
Only the directional derivative Du · h enters, and only on T.
The translation estimate in ∫⁻ form: for a C¹ function and 1 ≤ r,
∫ ‖u(x + h) - u(x)‖ ^ r dx ≤ ‖h‖ ^ r ∫ ‖Du‖ ^ r.
The local Lᵖ translation estimate: for a C¹ function and 1 ≤ p < ∞, if every
segment [x, x + h] starting in K lies in the measurable set T, then
‖u(· + h) - u‖_{Lᵖ(K)} ≤ ‖Du · h‖_{Lᵖ(T)}.
Unlike ContDiff.eLpNorm_comp_add_sub_le_mul_eLpNorm_fderiv, the right-hand side sees only the
derivative in the direction h, and only on T: this is the form in which translation increments
of a function defined on a domain are controlled away from the boundary.
The Lᵖ translation estimate: a C¹ function moves in Lᵖ at most linearly in the
translation, at the rate given by the Lᵖ seminorm of its derivative,
‖u(· + h) - u‖_p ≤ ‖h‖ ‖Du‖_p, 1 ≤ p < ∞.
No support, integrability or boundedness hypothesis is needed. For h ≠ 0, if Du is not in
Lᵖ the right-hand side is ∞ and the bound carries no information; at h = 0 both sides are
0.
Continuity of translation in Lᵖ for a C¹ function with Lᵖ derivative: the Lᵖ
distance between u and its translate tends to 0. This is the qualitative corollary of
ContDiff.eLpNorm_comp_add_sub_le_mul_eLpNorm_fderiv, which gives the linear modulus.
For a u that is itself in Lᵖ this is MeasureTheory.MemLp.tendsto_eLpNorm_comp_add_sub,
which needs no derivative; the content here is that a C¹ function with Lᵖ derivative
translates continuously in Lᵖ even when it is not in Lᵖ.