Scaling Haar measure by a continuous isomorphism

If G is a locally compact topological group and μ is a regular Haar measure on G, then an isomorphism φ : G ≃ₜ* G scales this measure by some positive real constant which we call mulEquivHaarChar φ.

Main definitions

• mulEquivHaarChar φ: the positive real such that (mulEquivHaarChar φ) • map φ μ = μ for μ a regular Haar measure.
• addEquivAddHaarChar φ: the additive version.

noncomputable def MeasureTheory.mulEquivHaarChar {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ* G) : NNReal

If φ : G ≃ₜ* G then mulEquivHaarChar φ is the positive real factor by which φ scales Haar measures on G.

Equations

• MeasureTheory.mulEquivHaarChar φ = MeasureTheory.Measure.haar.haarScalarFactor (MeasureTheory.Measure.map (⇑φ) MeasureTheory.Measure.haar)

noncomputable def MeasureTheory.addEquivAddHaarChar {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNReal

If φ : A ≃ₜ+ A then addEquivAddHaarChar φ is the positive real factor by which φ scales Haar measures on A.

Equations

• MeasureTheory.addEquivAddHaarChar φ = MeasureTheory.Measure.addHaar.addHaarScalarFactor (MeasureTheory.Measure.map (⇑φ) MeasureTheory.Measure.addHaar)

theorem MeasureTheory.mulEquivHaarChar_pos {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ* G) : 0 < mulEquivHaarChar φ

theorem MeasureTheory.addEquivAddHaarChar_pos {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : 0 < addEquivAddHaarChar φ

theorem MeasureTheory.mulEquivHaarChar_eq {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (φ : G ≃ₜ* G) : mulEquivHaarChar φ = μ.haarScalarFactor (Measure.map (⇑φ) μ)

theorem MeasureTheory.addEquivAddHaarChar_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : addEquivAddHaarChar φ = μ.addHaarScalarFactor (Measure.map (⇑φ) μ)

theorem MeasureTheory.mulEquivHaarChar_smul_map {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (φ : G ≃ₜ* G) : mulEquivHaarChar φ • Measure.map (⇑φ) μ = μ

theorem MeasureTheory.addEquivAddHaarChar_smul_map {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : addEquivAddHaarChar φ • Measure.map (⇑φ) μ = μ

theorem MeasureTheory.mulEquivHaarChar_smul_eq_comap {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] (φ : G ≃ₜ* G) : mulEquivHaarChar φ • μ = Measure.comap (⇑φ) μ

theorem MeasureTheory.addEquivAddHaarChar_smul_eq_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] (φ : G ≃ₜ+ G) : addEquivAddHaarChar φ • μ = Measure.comap (⇑φ) μ

theorem MeasureTheory.mulEquivHaarChar_smul_integral_map {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ* G) : mulEquivHaarChar φ • ∫ (a : G), f a ∂Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ

theorem MeasureTheory.addEquivAddHaarChar_smul_integral_map {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : addEquivAddHaarChar φ • ∫ (a : G), f a ∂Measure.map (⇑φ) μ = ∫ (a : G), f a ∂μ

theorem MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ* G) : ∫ (a : G), f a ∂Measure.comap (⇑φ) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ

theorem MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {f : G → ℝ} (φ : G ≃ₜ+ G) : ∫ (a : G), f a ∂Measure.comap (⇑φ) μ = addEquivAddHaarChar φ • ∫ (a : G), f a ∂μ

theorem MeasureTheory.mulEquivHaarChar_smul_preimage {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsHaarMeasure] [μ.Regular] {X : Set G} (φ : G ≃ₜ* G) : mulEquivHaarChar φ • μ (⇑φ ⁻¹' X) = μ X

theorem MeasureTheory.addEquivAddHaarChar_smul_preimage {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [μ.Regular] {X : Set G} (φ : G ≃ₜ+ G) : addEquivAddHaarChar φ • μ (⇑φ ⁻¹' X) = μ X

@[simp]

theorem MeasureTheory.mulEquivHaarChar_refl {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] : mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1

@[simp]

theorem MeasureTheory.addEquivAddHaarChar_refl {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] : addEquivAddHaarChar (ContinuousAddEquiv.refl G) = 1

theorem MeasureTheory.mulEquivHaarChar_trans {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {φ ψ : G ≃ₜ* G} : mulEquivHaarChar (ψ.trans φ) = mulEquivHaarChar ψ * mulEquivHaarChar φ

theorem MeasureTheory.addEquivAddHaarChar_trans {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {φ ψ : G ≃ₜ+ G} : addEquivAddHaarChar (ψ.trans φ) = addEquivAddHaarChar ψ * addEquivAddHaarChar φ