Conjugation-invariance in Lp, and the class functions #
Conjugation g ↦ h * g * h⁻¹ on a group is left translation followed by right translation, so a
measure that is invariant under both is invariant under conjugation. Normalized Haar measure on a
compact group is such a measure, which is what makes "class function" a meaningful condition on an
almost-everywhere equivalence class.
This file records that invariance as the two typeclasses Mathlib's machinery consumes: the
conjugation action of ConjAct G on G is measurable and measure-preserving, so
Mathlib's DomMulAct action supplies an isometric action of (ConjAct G)ᵈᵐᵃ on Lp E p μ by
precomposition, (c • f) g = f (h * g * h⁻¹). The class functions classFunctionLp are the
vectors that action fixes: a closed submodule, since each conjugation acts by an isometry.
Only conjugation-invariance, SMulInvariantMeasure (ConjAct G) G μ, is asked of μ for that
theory; two-sided translation invariance appears just once, as the hypothesis under which
TauCeti.instSMulInvariantMeasureConjAct supplies it.
The statements about the conjugation action itself (its measurability, its invariant measures and
its action on Lp) need only a DivInvMonoid, the level at which Mathlib defines that action;
the class functions are developed over a group.
The condition is on the class, not on a representative, and that is the point of packaging it
this way rather than as a pointwise slogan: pointwise conjugation-invariance of a function is not
stable under changing it on a null set, so it does not descend to Lp at all. What descends is
TauCeti.mem_classFunctionLp_iff_ae, invariance up to a null set.
Main definitions #
TauCeti.classFunctionLp: the class functions inLp E p μ, a submodule.TauCeti.conjLpₗᵢ: conjugation by a fixed element, as a linear isometric equivalence ofLp E p μ. This is the same operation as the(ConjAct G)ᵈᵐᵃ-action; forp = 2, the bundled linear isometry gives inner-product preservation throughLinearIsometry.inner_map_map.
Main statements #
TauCeti.instMeasurableConstSMulConjActandTauCeti.instSMulInvariantMeasureConjAct: the two instances that unlockDomMulAct's action onLp, the second deriving conjugation-invariance from two-sided translation invariance.TauCeti.measurePreserving_conj: conjugation preserves a conjugation-invariant measure, stated through the group operation.TauCeti.conjAct_smul_Lp_ae_eq: the induced action onLpis precomposition with conjugation.TauCeti.compMeasurePreserving_conj_eq_smul: precomposition with conjugation is that action.TauCeti.mem_classFunctionLp_iff_ae: membership read on representatives, as invariance almost everywhere.TauCeti.isClosed_classFunctionLp: the class functions are a closed subspace, hence (TauCeti.instCompleteSpaceClassFunctionLp) complete.TauCeti.mem_classFunctionLp_of_ae_eq_of_conj_invariant: a pointwise invariant representative makes a class function.TauCeti.conjLpₗᵢ_apply_of_mem_classFunctionLp: a class function is fixed by every conjugation isometry.
The compact-group specialization -- that the character of a continuous representation is a class
function in L²(G) -- is in TauCeti/RepresentationTheory/Compact/ClassFunctionLp.lean.
Conjugation by a fixed element is measurable, so the conjugation action of ConjAct G on G
has measurable orbit maps.
A two-sided invariant measure is invariant under conjugation.
Conjugation preserves a conjugation-invariant measure, stated in terms of the group
operation rather than the action of ConjAct G. Bi-invariant measures are the intended source of
the hypothesis (TauCeti.instSMulInvariantMeasureConjAct).
The action of (ConjAct G)ᵈᵐᵃ on Lp E p μ is precomposition with conjugation: the class of
f is sent to the class of g ↦ f (h * g * h⁻¹).
Precomposition by conjugation is the (ConjAct G)ᵈᵐᵃ-action.
The class functions in Lp. The submodule of Lp E p μ fixed by every conjugation,
for a conjugation-invariant measure μ on a group G.
Invariance is a condition on the class, not on a representative: an element of Lp is a class
function exactly when each of its conjugates agrees with it almost everywhere
(TauCeti.mem_classFunctionLp_iff_ae). Asking instead for a pointwise identity would not define a
submodule of Lp at all, since it is not stable under changing a representative on a null set.
Equations
Instances For
Membership of classFunctionLp is invariance under the action of (ConjAct G)ᵈᵐᵃ.
Membership of classFunctionLp, read on representatives. A class lies in
classFunctionLp exactly when each of its conjugates agrees with it almost everywhere.
The class functions form a closed subspace.
The class functions are complete. In particular classFunctionLp 𝕜 𝕜 2 μ is a Hilbert
space for RCLike 𝕜.
A genuinely invariant representative makes a class function. If some representative F of
f is constant on conjugacy classes on the nose, then f is a class function.
A constant is a class function.
Conjugation by a fixed element, as a linear isometric equivalence of Lp E p μ. It
agrees with the action of (ConjAct G)ᵈᵐᵃ (TauCeti.compMeasurePreserving_conj_eq_smul), is
represented by precomposition with conjugation (TauCeti.coeFn_conjLpₗᵢ), and its inverse is
conjugation by h⁻¹. For p = 2, the underlying linear isometry records inner-product
preservation through LinearIsometry.inner_map_map.
Equations
Instances For
Conjugation as an isometric equivalence applies by Lp.compMeasurePreserving.
The conjugation isometry is represented by g ↦ f (h * g * h⁻¹).
The inverse of conjugation by h is conjugation by h⁻¹.
A class function is fixed by every conjugation isometry. This is the definition of
TauCeti.classFunctionLp, read on the bundled operation.
On a commutative group every element of Lp is a class function: conjugation is trivial.