Documentation

Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

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) :

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)

Instances For

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

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)

Instances For

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 φ

theorem MeasureTheory.mulEquivHaarChar_symm {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {φ : G ≃ₜ* G} :

mulEquivHaarChar φ.symm = (mulEquivHaarChar φ)⁻¹

theorem MeasureTheory.addEquivAddHaarChar_symm {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] {φ : G ≃ₜ+ G} :

addEquivAddHaarChar φ.symm = (addEquivAddHaarChar φ)⁻¹

theorem MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ* G) :

mulEquivHaarChar φ = 1

theorem MeasureTheory.addEquivAddHaarChar_eq_one_of_compactSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ+ G) :

addEquivAddHaarChar φ = 1