The modular character: continuity, right translation and inversion

The modular character of a locally compact group is continuous. Its real value can be computed as the ratio of the integrals of a compactly supported continuous test function and its right translate. This supplies the continuous weight used in convolution involutions.

We use Mathlib's convention: right translation of the argument multiplies an integral by c(g) = Measure.modularCharacter g. This is the inverse of the modular function in Dana Williams, Crossed Products of C-Algebras*, Lemma 1.61.

For a Haar measure μ and a compactly supported continuous function f with values in a real normed space, we prove the right-translation formula ∫ f (x * g) dμ = c(g) • ∫ f dμ and the inversion formula ∫ f x⁻¹ dμ = ∫ c(x) • f x dμ, equivalently ∫ c(x) • f x⁻¹ dμ = ∫ f dμ. These need no regularity, countability or σ-finiteness of μ. For an inner regular Haar measure we deduce the measure identity μ.inv = μ.withDensity c; inversion of a left Haar measure thus has the continuous, strictly positive density c. These are the change-of-variables formulas behind the twisted involution f*(s) = c(s) α_s(f(s⁻¹)*) of crossed-product convolution algebras.

The same identities hold for a regular Haar measure, which need not be inner regular when the group is not σ-compact; the canonical MeasureTheory.Measure.haar is regular. Mathlib's right-translation identity map (· * g) μ = c(g) • μ assumes inner regularity; for a regular μ it follows from uniqueness of regular left invariant measures, since right translation is a homeomorphism and preserves regularity. For the inversion formula, (μ.withDensity c).inv is a left Haar measure agreeing with μ on compact sets, hence on open sets, and outer regularity of μ compares the two on all sets. Consequently right translation and inversion preserve null sets of a regular Haar measure, and both change-of-variables formulas hold for every integrand. Unlike Mathlib's MeasureTheory.measure_inv_null and MeasureTheory.quasiMeasurePreserving_mul_right, none of this assumes σ-finiteness.

Main statements

• TauCeti.integral_mul_right_eq_modularCharacter_smul: right translation of compactly supported integrands.
• TauCeti.integral_modularCharacter_smul_inv_eq_self and TauCeti.integral_inv_eq_integral_modularCharacter_smul: the inversion formula on compactly supported integrands.
• MeasureTheory.Measure.isMulRightInvariant_withDensity_modularCharacter: μ.withDensity c is right invariant for an inner regular Haar measure μ.
• MeasureTheory.Measure.inv_eq_withDensity_modularCharacter: μ.inv = μ.withDensity c for an inner regular Haar measure μ.
• MeasureTheory.Measure.map_right_mul_eq_modularCharacter_smul_of_regular: map (· * g) μ = c(g) • μ for a regular Haar measure μ.
• MeasureTheory.Measure.inv_eq_withDensity_modularCharacter_of_regular: μ.inv = μ.withDensity c for a regular Haar measure μ.
• MeasureTheory.Measure.quasiMeasurePreserving_mul_right_of_regular, MeasureTheory.Measure.quasiMeasurePreserving_inv_of_regular and MeasureTheory.Measure.quasiMeasurePreserving_inv_mul_of_regular: right translation, inversion and y ↦ y⁻¹ * x preserve null sets of a regular Haar measure.
• TauCeti.integral_mul_right_eq_modularCharacter_smul_of_regular, TauCeti.integral_inv_eq_integral_modularCharacter_smul_of_regular and their lower Lebesgue versions TauCeti.lintegral_mul_right_eq_modularCharacter_mul_of_regular and TauCeti.lintegral_inv_eq_lintegral_modularCharacter_mul_of_regular: the change-of-variables formulas for every integrand, against a regular Haar measure.

References

• Dana Williams, Crossed Products of C-Algebras*, Lemma 1.61, for the modular function and the inversion formula in the convention Δ = c⁻¹.

theorem TauCeti.modularCharacter_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (g : G) : MeasureTheory.Measure.modularCharacter g = MeasureTheory.Measure.modularCharacterFun g

The bundled modular character evaluates to the modular character function.

theorem TauCeti.modularCharacter_eq_integral_div {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] {f : G → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) (hfi : ∫ (x : G), f x ∂μ ≠ 0) (g : G) : ↑(MeasureTheory.Measure.modularCharacter g) = (∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂μ

A nonzero test integral computes the modular character by right translation. No regularity assumption on the Haar measure is needed.

theorem TauCeti.continuous_modularCharacter {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] : Continuous ⇑MeasureTheory.Measure.modularCharacter

The modular character is continuous, without countability or separation assumptions.

theorem TauCeti.modularCharacter_rpow_mul_inv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (r : ℝ) (x : G) : ↑(MeasureTheory.Measure.modularCharacter x) ^ r * ↑(MeasureTheory.Measure.modularCharacter x⁻¹) ^ r = 1

The real powers c(x)^r and c(x⁻¹)^r of the modular character multiply to one.

theorem TauCeti.modularCharacter_mul_inv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (x : G) : ↑(MeasureTheory.Measure.modularCharacter x) * ↑(MeasureTheory.Measure.modularCharacter x⁻¹) = 1

The values c(x) and c(x⁻¹) of the modular character multiply to one.

theorem TauCeti.modularCharacter_mul_inv_cancel_right {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (x y : G) : ↑(MeasureTheory.Measure.modularCharacter (x * y)) * ↑(MeasureTheory.Measure.modularCharacter y⁻¹) = ↑(MeasureTheory.Measure.modularCharacter x)

The values c(x * y) and c(y⁻¹) of the modular character multiply to c(x).

theorem TauCeti.integral_mul_right_eq_modularCharacter_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] {f : G → E} (hf : Continuous f) (hfc : HasCompactSupport f) (g : G) : ∫ (x : G), f (x * g) ∂μ = ↑(MeasureTheory.Measure.modularCharacter g) • ∫ (x : G), f x ∂μ

Right translation of a compactly supported integrand multiplies its Haar integral by the modular character. No regularity of the Haar measure is needed.

theorem TauCeti.integral_modularCharacter_smul_inv_eq_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] {f : G → E} (hf : Continuous f) (hfc : HasCompactSupport f) : ∫ (x : G), ↑(MeasureTheory.Measure.modularCharacter x) • f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ

The inversion formula for a compactly supported integrand, in the form used by the twisted involution f*(x) = c(x) f(x⁻¹): weighting by the modular character makes inversion preserve Haar integrals. No regularity of the Haar measure is needed.

theorem TauCeti.integral_inv_eq_integral_modularCharacter_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] {f : G → E} (hf : Continuous f) (hfc : HasCompactSupport f) : ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), ↑(MeasureTheory.Measure.modularCharacter x) • f x ∂μ

The inversion formula for a compactly supported integrand: inverting the argument weights a Haar integral by the modular character. No regularity of the Haar measure is needed.

theorem MeasureTheory.Measure.isMulRightInvariant_withDensity_modularCharacter {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.InnerRegular] : (μ.withDensity fun (x : G) => ↑(modularCharacter x)).IsMulRightInvariant

Weighting an inner regular Haar measure by the modular character gives a right invariant measure.

theorem MeasureTheory.Measure.inv_eq_withDensity_modularCharacter {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.InnerRegular] : μ.inv = μ.withDensity fun (x : G) => ↑(modularCharacter x)

The inversion formula for an inner regular Haar measure: the inverse measure μ.inv, that is μ.map Inv.inv, has density modularCharacter with respect to μ.

theorem MeasureTheory.Measure.map_right_mul_eq_modularCharacter_smul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (g : G) : map (fun (x : G) => x * g) μ = modularCharacter g • μ

Right translation of a regular Haar measure multiplies it by the modular character. This is the counterpart, for regular instead of inner regular Haar measures, of Mathlib's MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul.

theorem MeasureTheory.Measure.measure_preimage_mul_right_eq_modularCharacter_mul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (g : G) (s : Set G) : μ ((fun (x : G) => x * g) ⁻¹' s) = ↑(modularCharacter g) * μ s

Right translation scales the measure of every set, measurable or not, by the modular character of a regular Haar measure.

theorem MeasureTheory.Measure.measure_mul_right_null_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (g : G) {s : Set G} : μ ((fun (x : G) => x * g) ⁻¹' s) = 0 ↔ μ s = 0

Right translation preserves null sets of a regular Haar measure.

theorem MeasureTheory.Measure.quasiMeasurePreserving_mul_right_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (g : G) : QuasiMeasurePreserving (fun (x : G) => x * g) μ μ

Right translation is quasi-measure-preserving for a regular Haar measure.

theorem MeasureTheory.Measure.isMulRightInvariant_withDensity_modularCharacter_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] : (μ.withDensity fun (x : G) => ↑(modularCharacter x)).IsMulRightInvariant

Weighting a regular Haar measure by the modular character gives a right invariant measure.

theorem MeasureTheory.Measure.inv_eq_withDensity_modularCharacter_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] : μ.inv = μ.withDensity fun (x : G) => ↑(modularCharacter x)

The inversion formula for a regular Haar measure: the inverse measure μ.inv, that is μ.map Inv.inv, has density modularCharacter with respect to μ. No inner regularity or σ-finiteness of μ is assumed.

theorem MeasureTheory.Measure.inv_absolutelyContinuous_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] : μ.inv.AbsolutelyContinuous μ

Inversion maps null sets of a regular Haar measure to null sets: μ.inv ≪ μ. Mathlib's MeasureTheory.inv_absolutelyContinuous needs σ-finiteness instead of regularity.

theorem MeasureTheory.Measure.absolutelyContinuous_inv_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] : μ.AbsolutelyContinuous μ.inv

A regular Haar measure is absolutely continuous with respect to its inverse.

@[simp]

theorem MeasureTheory.Measure.measure_inv_null_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] {s : Set G} : μ s⁻¹ = 0 ↔ μ s = 0

Inversion preserves null sets of a regular Haar measure.

theorem MeasureTheory.Measure.quasiMeasurePreserving_inv_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] : QuasiMeasurePreserving Inv.inv μ μ

Inversion is quasi-measure-preserving for a regular Haar measure.

theorem MeasureTheory.Measure.quasiMeasurePreserving_inv_mul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (x : G) : QuasiMeasurePreserving (fun (y : G) => y⁻¹ * x) μ μ

For a regular Haar measure, y ↦ y⁻¹ * x is quasi-measure-preserving: it is inversion followed by right translation by x.

theorem TauCeti.lintegral_mul_right_eq_modularCharacter_mul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] [μ.Regular] (f : G → ENNReal) (g : G) : ∫⁻ (x : G), f (x * g) ∂μ = ↑(MeasureTheory.Measure.modularCharacter g) * ∫⁻ (x : G), f x ∂μ

Right translation of a lower Lebesgue integral against a regular Haar measure multiplies it by the modular character, for every integrand.

theorem TauCeti.lintegral_inv_eq_lintegral_modularCharacter_mul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] [μ.Regular] (f : G → ENNReal) : ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), ↑(MeasureTheory.Measure.modularCharacter x) * f x ∂μ

The inversion formula for a regular Haar measure: inverting the argument weights the lower Lebesgue integral by the modular character, for every integrand.

theorem TauCeti.integral_mul_right_eq_modularCharacter_smul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] [μ.Regular] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : G → E) (g : G) : ∫ (x : G), f (x * g) ∂μ = ↑(MeasureTheory.Measure.modularCharacter g) • ∫ (x : G), f x ∂μ

Right translation of a Bochner integral against a regular Haar measure multiplies it by the modular character, for every integrand.

theorem TauCeti.integral_inv_eq_integral_modularCharacter_smul_of_regular {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure] [μ.Regular] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : G → E) : ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), ↑(MeasureTheory.Measure.modularCharacter x) • f x ∂μ

The inversion formula for a regular Haar measure: inverting the argument weights the Bochner integral by the modular character, for every integrand.