Documentation

TauCeti.MeasureTheory.Function.Lp.LeftTranslation

Left translation on Lᵖ of a group #

Let μ be a left-invariant measure on a group G. Left translation of functions,

(L_g f)(x) = f (g⁻¹ * x),        L_g L_h = L_(g * h),

preserves Lᵖ classes and norms, so it gives a group homomorphism MeasureTheory.Lp.leftTranslation μ p 𝕜 : G →* (Lp E p μ ≃ₗᵢ[𝕜] Lp E p μ). It is the action of DomMulAct.mk g⁻¹ from Mathlib's DomMulAct action on Lp, reindexed so that it is a left action of G itself. For p < ∞ and a locally finite measure that is inner regular for compact sets, such as a regular Haar measure, Mathlib's continuity of that action makes left translation strongly continuous.

For real-valued functions, left translation is an order automorphism, preserves integrals and fixes the constant class one of L∞. The class of the left translate of a bounded continuous function is the left translate of its class, so BoundedContinuousFunction.toLpTop is equivariant. These are the translation-invariance properties needed to compare invariant means on bounded uniformly continuous functions with invariant means on L∞ of a Haar measure.

Main definitions #

Main results #

source
def MeasureTheory.Lp.leftTranslation {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] [NormedAddCommGroup E] (p : ENNReal) [Fact (1 ≤ p)] (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] :
G →* ↥(Lp E p μ) ≃ₗᵢ[𝕜] ↥(Lp E p μ)

Left translation g ↦ L_g on Lp E p μ for a left-invariant measure μ, where (L_g f)(x) = f (g⁻¹ * x), as a group homomorphism to linear isometry equivalences.

Instances For
    source
    theorem MeasureTheory.Lp.leftTranslation_apply {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (g : G) (f : ↥(Lp E p μ)) :
    ((leftTranslation μ p 𝕜) g) f = DomMulAct.mk g⁻¹ • f

    Left translation by g is the DomMulAct action of g⁻¹.

    source
    theorem MeasureTheory.Lp.coeFn_leftTranslation {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (g : G) (f : ↥(Lp E p μ)) :
    ↑↑(((leftTranslation μ p 𝕜) g) f) =ᵐ[μ] fun (x : G) => ↑↑f (g⁻¹ * x)

    The left translate L_g f is almost everywhere the function x ↦ f (g⁻¹ * x).

    source
    @[simp]
    theorem MeasureTheory.Lp.leftTranslation_symm {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (g : G) :
    ((leftTranslation μ p 𝕜) g).symm = (leftTranslation μ p 𝕜) g⁻¹

    The inverse of left translation by g is left translation by g⁻¹.

    source
    theorem MeasureTheory.Lp.leftTranslation_mono {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] {p : ENNReal} [Fact (1 ≤ p)] (g : G) {f f' : ↥(Lp ℝ p μ)} (h : f ≤ f') :
    ((leftTranslation μ p ℝ) g) f ≤ ((leftTranslation μ p ℝ) g) f'

    Left translation is monotone on real Lᵖ.

    source
    @[simp]
    theorem MeasureTheory.Lp.leftTranslation_le_leftTranslation_iff {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] {p : ENNReal} [Fact (1 ≤ p)] {g : G} {f f' : ↥(Lp ℝ p μ)} :
    ((leftTranslation μ p ℝ) g) f ≤ ((leftTranslation μ p ℝ) g) f' ↔ f ≤ f'

    Left translation is an order automorphism of real Lᵖ.

    source
    @[simp]
    theorem MeasureTheory.Lp.leftTranslation_one {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] (g : G) :
    ((leftTranslation μ ⊤ ℝ) g) 1 = 1

    Left translation fixes the constant class one of L∞.

    source
    @[simp]
    theorem MeasureTheory.Lp.integral_leftTranslation {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] (g : G) (f : ↥(Lp E p μ)) :
    ∫ (x : G), ↑↑(((leftTranslation μ p 𝕜) g) f) x ∂μ = ∫ (x : G), ↑↑f x ∂μ

    Left translation preserves the integral of an Lᵖ class, since μ is left invariant.

    source
    theorem MeasureTheory.Lp.leftTranslation_toLpTop {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [SecondCountableTopologyEither G E] (g : G) (f : BoundedContinuousFunction G E) :
    ((leftTranslation μ ⊤ 𝕜) g) ((BoundedContinuousFunction.toLpTop μ 𝕜) f) = (BoundedContinuousFunction.toLpTop μ 𝕜) (f.compContinuous (ContinuousMap.mulLeft g⁻¹))

    The class in L∞ of the left translate x ↦ f (g⁻¹ * x) of a bounded continuous function is the left translate of its class.

    source
    theorem MeasureTheory.Lp.continuous_leftTranslation_apply {G : Type u_1} {E : Type u_2} [Group G] [MeasurableSpace G] [MeasurableMul G] {μ : Measure G} [μ.IsMulLeftInvariant] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop] (hp : p ≠ ⊤) (f : ↥(Lp E p μ)) :
    Continuous fun (g : G) => ((leftTranslation μ p 𝕜) g) f

    For p < ∞, left translation on Lᵖ is strongly continuous: g ↦ L_g f is continuous for every f, when μ is locally finite and inner regular for compact sets, as a regular Haar measure is.

    source
    @[simp]
    theorem MeasureTheory.Lp.leftTranslation_linftyIndicator {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] {ν : Measure G} [ν.IsMulLeftInvariant] (g : G) {s : Set G} (hs : MeasurableSet s) :
    ((leftTranslation ν ⊤ ℝ) g) (TauCeti.linftyIndicator ν s hs) = TauCeti.linftyIndicator ν (g • s) ⋯

    Left translation by g of the indicator of s in L∞ is the indicator of g • s.