Right translation on Lᵖ of a locally compact group #
Let μ be a regular left Haar measure on a locally compact group G, and write
c = MeasureTheory.Measure.modularCharacter, so that ∫ f (x * g) dμ = c(g) ∫ f dμ. Right
translation x ↦ x * g scales ‖·‖_p ^ p by c(g), so the weighted right translation
(R_g f)(x) = c(g⁻¹)^(1/p) • f (x * g), R_g R_h = R_(g * h),
is an isometry of Lᵖ, with the convention 1/∞ = 0. On L¹ it is f ↦ c(g⁻¹) • f (· * g).
Unlike left translation, it is not given by a measure-preserving map unless G is unimodular.
We obtain it by conjugating left translation with the modular inversion
(J f)(x) = c(x)^(1/p) • f x⁻¹,
which is an isometric involution of Lᵖ by the inversion formula μ.inv = μ.withDensity c.
Indeed J L_g J = R_g, so right translation inherits from left translation the group law and,
for p < ∞, strong continuity: each orbit g ↦ R_g f is continuous. By left invariance and
the inversion formula, the convolution (h ⋆ k)(x) = ∫ y, h y * k (y⁻¹ * x) dμ of L¹
functions is ∫ z, k z * c(z) * h (x * z⁻¹) dμ, an average of the right translates
R_(z⁻¹) h of h weighted by k. Strong continuity of right translation on L¹ is therefore
the input for showing that convolution on the right with kernels concentrated near the
identity approximates h.
No σ-finiteness of μ and no countability of G is assumed.
Main definitions #
MeasureTheory.Lp.modularInversion μ p 𝕜: the isometric involutionf ↦ (x ↦ c(x)^(1/p) • f x⁻¹)ofLp E p μ.MeasureTheory.Lp.rightTranslation μ p 𝕜: right translationg ↦ R_gonLp E p μ, as a group homomorphism to linear isometry equivalences.
Main results #
TauCeti.eLpNorm_modularCharacter_rpow_smul_comp_inv: the weighted inversion preserves theLᵖseminorm.MeasureTheory.Lp.coeFn_modularInversion,MeasureTheory.Lp.coeFn_rightTranslation: the pointwise formulas, almost everywhere.MeasureTheory.Lp.modularInversion_modularInversion: the modular inversion is an involution.MeasureTheory.Lp.leftTranslation_rightTranslation: left and right translations commute.MeasureTheory.Lp.modularInversion_le_modularInversion_iff,MeasureTheory.Lp.rightTranslation_le_rightTranslation_iff: the modular inversion and right translation are order automorphisms of realLᵖ.MeasureTheory.Lp.integral_modularInversion,MeasureTheory.Lp.integral_rightTranslation: onL¹they preserve the integral.MeasureTheory.Lp.modularInversion_toL1: onL¹, the modular inversion of a compactly supported continuous function is the class ofx ↦ c(x) • f x⁻¹.MeasureTheory.Lp.continuous_rightTranslation_apply: right translation is strongly continuous forp < ∞, soR_(g⁻¹) f → fasg → 1(MeasureTheory.Lp.tendsto_rightTranslation_inv).MeasureTheory.Lp.integrable_smul_rightTranslation_inv: the weighted orbitz ↦ k z • R_(z⁻¹) hofh ∈ L¹is integrable for an integrable weightk.MeasureTheory.eLpNorm_comp_mul_right_of_regular: the unweighted right translate satisfies‖f (· * g)‖_p = c(g)^(1/p) ‖f‖_p.MeasureTheory.MemLp.tendsto_eLpNorm_comp_mul_right_sub_of_regular:‖f (· * g) - f‖_p → 0asg → 1, for1 ≤ p < ∞.
References #
- G. B. Folland, A Course in Abstract Harmonic Analysis, §§2.4–2.5, for the modular function
and the continuity of translations in
Lᵖ. - B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix A.3.
The weighted inversion x ↦ c(x)^r • f x⁻¹ of an almost everywhere strongly measurable
function is almost everywhere strongly measurable.
The weighted inversion x ↦ c(x) • f x⁻¹ of a continuous function is continuous.
The weighted inversion x ↦ c(x) • f x⁻¹ of a compactly supported function is compactly
supported.
The weighted inversion x ↦ c(x)^(1/p) • f x⁻¹ preserves the Lᵖ seminorm of an almost
everywhere strongly measurable function, for a regular Haar measure.
The weighted inversion x ↦ c(x)^(1/p) • f x⁻¹ of an Lᵖ function is in Lᵖ, for a regular
Haar measure.
The modular inversion (J f)(x) = c(x)^(1/p) • f x⁻¹ on Lp E p μ for a regular Haar
measure μ, where c is the modular character and 1/∞ = 0. It is a linear isometric
involution.
Instances For
The modular inversion J f is almost everywhere the function x ↦ c(x)^(1/p) • f x⁻¹.
The modular inversion is an involution.
The modular inversion is its own inverse.
The modular inversion squares to the identity in the group of linear isometry equivalences.
Right translation g ↦ R_g on Lp E p μ for a regular Haar measure μ, where
(R_g f)(x) = c(g⁻¹)^(1/p) • f (x * g), c is the modular character and 1/∞ = 0, as a group
homomorphism to linear isometry equivalences. It is the conjugate J L_g J of left translation
by the modular inversion J.
Instances For
Right translation is left translation conjugated by the modular inversion.
The right translate R_g f is almost everywhere the function
x ↦ c(g⁻¹)^(1/p) • f (x * g).
The inverse of right translation by g is right translation by g⁻¹.
Left and right translations commute.
Right translation is monotone on real Lᵖ.
Right translation is an order automorphism of real Lᵖ.
The modular inversion is monotone on real Lᵖ.
The modular inversion is an order automorphism of real Lᵖ.
The modular inversion on L¹ preserves the integral: ∫ x, c(x) • f x⁻¹ dμ = ∫ f dμ.
The modular inversion of the L¹ class of a compactly supported continuous function f is the
class of x ↦ c(x) • f x⁻¹.
Right translation on L¹ preserves the integral: the weight c(g⁻¹) of
(R_g f)(x) = c(g⁻¹) • f (x * g) compensates the factor c(g) by which right translation scales
the integral.
Right translation is strongly continuous on Lᵖ for p < ∞: every orbit map
g ↦ R_g f is continuous.
The right translates R_(g⁻¹) f tend to f in Lᵖ as g → 1, for p < ∞.
For an integrable weight k and h ∈ L¹(G, μ), the weighted orbit z ↦ k z • R_(z⁻¹) h is
integrable; its integral is the convolution h ⋆ k when E = ℝ.
The unweighted right translate f (· * g) has Lᵖ seminorm c(g)^(1/p) ‖f‖_p, where c is
the modular character, for every function and every exponent.
The unweighted right translate of an Lᵖ function is in Lᵖ.
A function is in Lᵖ exactly when its unweighted right translate is.
The unweighted right translates of an Lᵖ function converge to it in Lᵖ for
1 ≤ p < ∞: ‖f (· * g) - f‖_p → 0 as g → 1. This is the counterpart for a regular left
Haar measure of MeasureTheory.MemLp.tendsto_eLpNorm_comp_add_sub in
TauCeti/MeasureTheory/Function/Lp/Translation.lean.