Documentation

TauCeti.MeasureTheory.Group.Inversion

Precomposition with inversion on Lp of a group #

A measure on a type with involutive inversion that is invariant under inversion — normalized Haar measure on a compact group, for instance — makes g ↦ g⁻¹ measure preserving, so precomposition with it is a linear isometric equivalence of Lp E p μ. Inversion is an involution, so this equivalence is its own inverse: an element of Lp vanishes exactly when its inverse-translate does.

The construction is MeasureTheory.Lp.compMeasurePreservingₗᵢEquiv (TauCeti/MeasureTheory/Function/Lp/CompMeasurePreservingEquiv.lean) at the inverse pair Inv.inv, Inv.inv; what this file adds is the interaction with the class functions of TauCeti/MeasureTheory/Group/Conjugation.lean and the compatibility with the continuous functions that supply the elements of Lp in practice.

The intended use is the change of variables ∫ f g⁻¹ dg = ∫ f g dg in inner-product form: for p equal to 2 this map preserves the inner product, which is what turns a statement about a function into the corresponding statement about its inverse-translate.

Main definitions #

Main statements #

source
noncomputable def TauCeti.invLpₗᵢ {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] :
↥(MeasureTheory.Lp E p μ) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp E p μ)

Precomposition with inversion on Lp, for a measure invariant under inversion. It is a linear isometric equivalence because g ↦ g⁻¹ preserves μ and is its own inverse.

Equations
Instances For
    source
    theorem TauCeti.invLpₗᵢ_apply {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] (f : ↥(MeasureTheory.Lp E p μ)) :
    (invLpₗᵢ 𝕜) f = (MeasureTheory.Lp.compMeasurePreserving Inv.inv ⋯) f

    The inversion equivalence is precomposition with Inv.inv.

    Not a simp lemma: unfolding to Lp.compMeasurePreserving dissolves the abstraction, and it would take TauCeti.invLpₗᵢ_invLpₗᵢ out of simp normal form (the simpNF linter rejects the pair). Use it to rewrite by hand where the underlying precomposition is wanted.

    source
    theorem TauCeti.coeFn_invLpₗᵢ {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] (f : ↥(MeasureTheory.Lp E p μ)) :
    ↑↑((invLpₗᵢ 𝕜) f) =ᵐ[μ] fun (g : G) => ↑↑f g⁻¹

    The inverse-translate of a class of functions is represented by g ↦ f g⁻¹.

    source
    @[simp]
    theorem TauCeti.invLpₗᵢ_invLpₗᵢ {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] (f : ↥(MeasureTheory.Lp E p μ)) :
    (invLpₗᵢ 𝕜) ((invLpₗᵢ 𝕜) f) = f

    Inverting twice is the identity. The two precompositions compose to precomposition with g ↦ (g⁻¹)⁻¹, which is the identity on the nose.

    source
    @[simp]
    theorem TauCeti.invLpₗᵢ_symm {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] :
    (invLpₗᵢ 𝕜).symm = invLpₗᵢ 𝕜

    The inversion equivalence is its own inverse: it is an equivalence and an involution.

    source
    theorem TauCeti.invLpₗᵢ_mem_classFunctionLp {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Group G] [MeasurableInv G] [μ.IsInvInvariant] [MeasurableMul G] [MeasureTheory.SMulInvariantMeasure (ConjAct G) G μ] {f : ↥(MeasureTheory.Lp E p μ)} (hf : f ∈ classFunctionLp 𝕜 E p μ) :
    (invLpₗᵢ 𝕜) f ∈ classFunctionLp 𝕜 E p μ

    Inversion preserves the class functions. Conjugation commutes with inversion, (h * g * h⁻¹)⁻¹ = h * g⁻¹ * h⁻¹, so the conjugates of the inverse-translate of f are the inverse-translates of the conjugates of f.

    source
    theorem TauCeti.invLpₗᵢ_mem_classFunctionLp_iff {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Group G] [MeasurableInv G] [μ.IsInvInvariant] [MeasurableMul G] [MeasureTheory.SMulInvariantMeasure (ConjAct G) G μ] {f : ↥(MeasureTheory.Lp E p μ)} :
    (invLpₗᵢ 𝕜) f ∈ classFunctionLp 𝕜 E p μ ↔ f ∈ classFunctionLp 𝕜 E p μ

    Inversion reflects the class functions. Preservation both ways, since inversion is an involution: the inverse-translate of f is a class function exactly when f is one.

    Not a simp lemma: TauCeti.mem_classFunctionLp_iff already rewrites the left-hand side to the invariance condition, so simp never reaches this one (the simpNF linter rejects it).

    source
    theorem TauCeti.invLpₗᵢ_toLp {G : Type u_1} {E : Type u_2} [MeasurableSpace G] [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)] {μ : MeasureTheory.Measure G} (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [InvolutiveInv G] [MeasurableInv G] [μ.IsInvInvariant] [TopologicalSpace G] [ContinuousInv G] [CompactSpace G] [BorelSpace G] [SecondCountableTopologyEither G E] [MeasureTheory.IsFiniteMeasure μ] (F : C(G, E)) :
    (invLpₗᵢ 𝕜) ((ContinuousMap.toLp p μ 𝕜) F) = (ContinuousMap.toLp p μ 𝕜) (F.comp { toFun := Inv.inv, continuous_toFun := ⋯ })

    On a continuous function, inversion on Lp is precomposition with inversion.