Haar measures on group extensions

In this file, if 1 → A → B → C → 1 is a short exact sequence of topological groups, we construct a Haar measure on B from Haar measures on A and C.

Main definitions

• TopologicalGroup.IsSES.inducedMeasure: The Haar measure on B induced by Haar measures on A and C.

Main results

• TopologicalGroup.IsSES.isHaarMeasure_inducedMeasure: inducedMeasure is a Haar measure.
• TopologicalGroup.IsSES.inducedMeasure_lt_of_injOn: If ψ is injective on an open set U, then the induced measure on U is bounded by μC Set.univ * μA {1} (possibly infinite).

@[reducible, inline]

noncomputable abbrev TopologicalGroup.IsSES.pullback {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B) : CompactlySupportedContinuousMap A E

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, then we can pull back a continuous compactly supported function f on B along φ to the continuous compactly supported function a ↦ f (b * φ a) on A.

Equations

• H.pullback f b = CompactlySupportedContinuousMap.pullback_monoidHom ⋯ f b

@[reducible, inline]

noncomputable abbrev TopologicalAddGroup.IsSES.pullback {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B) : CompactlySupportedContinuousMap A E

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive topological groups, then we can pull back a continuous compactly supported function f on B along φ to the continuous compactly supported function a ↦ f (b + φ a) on A.

Equations

• H.pullback f b = CompactlySupportedContinuousMap.pullback_addMonoidHom ⋯ f b

theorem TopologicalGroup.IsSES.pullback_def {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B) (a : A) : (H.pullback f b) a = f (b * φ a)

theorem TopologicalAddGroup.IsSES.pullback_def {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] (f : CompactlySupportedContinuousMap B E) (b : B) (a : A) : (H.pullback f b) a = f (b + φ a)

theorem TopologicalGroup.IsSES.integral_pullback_invFun_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] (f : CompactlySupportedContinuousMap B E) (b : B) : ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

theorem TopologicalAddGroup.IsSES.integral_pullback_invFun_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] (f : CompactlySupportedContinuousMap B E) (b : B) : ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA

noncomputable def TopologicalGroup.IsSES.pushforward {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] [IsTopologicalGroup C] [LocallyCompactSpace B] : CompactlySupportedContinuousMap B E →ₗ[ℝ] CompactlySupportedContinuousMap C E

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, then we can push forward a continuous compactly supported function on B to a continuous compactly supported function on C by integrating over A.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TopologicalAddGroup.IsSES.pushforward {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] [IsTopologicalAddGroup C] [LocallyCompactSpace B] : CompactlySupportedContinuousMap B E →ₗ[ℝ] CompactlySupportedContinuousMap C E

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive topological groups, then we can push forward a continuous compactly supported function on B to a continuous compactly supported function on C by integrating over A.

Equations

• One or more equations did not get rendered due to their size.

theorem TopologicalGroup.IsSES.pushforward_def {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] [IsTopologicalGroup C] [LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (c : C) : ((H.pushforward μA) f) c = ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

theorem TopologicalAddGroup.IsSES.pushforward_def {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] [IsTopologicalAddGroup C] [LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (c : C) : ((H.pushforward μA) f) c = ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

theorem TopologicalGroup.IsSES.pushforward_apply_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] [IsTopologicalGroup C] [LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (b : B) : ((H.pushforward μA) f) (ψ b) = ∫ (a : A), (H.pullback f b) a ∂μA

theorem TopologicalAddGroup.IsSES.pushforward_apply_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] [IsTopologicalAddGroup C] [LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (b : B) : ((H.pushforward μA) f) (ψ b) = ∫ (a : A), (H.pullback f b) a ∂μA

theorem TopologicalGroup.IsSES.pushforward_mono {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤ g) : (H.pushforward μA) f ≤ (H.pushforward μA) g

theorem TopologicalAddGroup.IsSES.pushforward_mono {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤ g) : (H.pushforward μA) f ≤ (H.pushforward μA) g

noncomputable def TopologicalGroup.IsSES.integrate {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] : CompactlySupportedContinuousMap B E →ₗ[ℝ] E

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, then we can integrate a continuous compactly supported function on B by integrating over A and C.

Equations

• H.integrate μA μC = { toFun := fun (f : CompactlySupportedContinuousMap B E) => ∫ (c : C), ((H.pushforward μA) f) c ∂μC, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def TopologicalAddGroup.IsSES.integrate {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] : CompactlySupportedContinuousMap B E →ₗ[ℝ] E

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive topological groups, then we can integrate a continuous compactly supported function on B by integrating over A and C.

Equations

• H.integrate μA μC = { toFun := fun (f : CompactlySupportedContinuousMap B E) => ∫ (c : C), ((H.pushforward μA) f) c ∂μC, map_add' := ⋯, map_smul' := ⋯ }

theorem TopologicalGroup.IsSES.integrate_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [NormedSpace ℝ E] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] (f : CompactlySupportedContinuousMap B E) : (H.integrate μA μC) f = ∫ (c : C), ((H.pushforward μA) f) c ∂μC

theorem TopologicalAddGroup.IsSES.integrate_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [NormedAddCommGroup E] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [NormedSpace ℝ E] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] (f : CompactlySupportedContinuousMap B E) : (H.integrate μA μC) f = ∫ (c : C), ((H.pushforward μA) f) c ∂μC

theorem TopologicalGroup.IsSES.integrate_mono {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤ g) : (H.integrate μA μC) f ≤ (H.integrate μA μC) g

theorem TopologicalAddGroup.IsSES.integrate_mono {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] {f g : CompactlySupportedContinuousMap B ℝ} (h : f ≤ g) : (H.integrate μA μC) f ≤ (H.integrate μA μC) g

noncomputable def TopologicalGroup.IsSES.inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : MeasureTheory.Measure B

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, then we can define a Haar measure on B induced by the Haar measures on A and C.

Equations

• H.inducedMeasure μA μC = RealRMK.rieszMeasure { toLinearMap := H.integrate μA μC, monotone' := ⋯ }

noncomputable def TopologicalAddGroup.IsSES.inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : MeasureTheory.Measure B

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive topological groups, then we can define a Haar measure on B induced by the Haar measures on A and C.

Equations

• H.inducedMeasure μA μC = RealRMK.rieszMeasure { toLinearMap := H.integrate μA μC, monotone' := ⋯ }

instance TopologicalGroup.IsSES.inducedMeasure_regular {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : (H.inducedMeasure μA μC).Regular

instance TopologicalAddGroup.IsSES.inducedMeasure_regular {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : (H.inducedMeasure μA μC).Regular

theorem TopologicalGroup.IsSES.integral_inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] (f : CompactlySupportedContinuousMap B ℝ) : ∫ (b : B), f b ∂H.inducedMeasure μA μC = (H.integrate μA μC) f

theorem TopologicalAddGroup.IsSES.integral_inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] (f : CompactlySupportedContinuousMap B ℝ) : ∫ (b : B), f b ∂H.inducedMeasure μA μC = (H.integrate μA μC) f

instance TopologicalGroup.IsSES.isHaarMeasure_inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : (H.inducedMeasure μA μC).IsHaarMeasure

instance TopologicalAddGroup.IsSES.isAddHaarMeasure_inducedMeasure {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] : (H.inducedMeasure μA μC).IsAddHaarMeasure

theorem TopologicalGroup.IsSES.inducedMeasure_lt_of_injOn {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →* B} {ψ : B →* C} (H : IsSES φ ψ) [IsTopologicalGroup A] [IsTopologicalGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsHaarMeasure] [IsTopologicalGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] {U : Set B} (hU : IsOpen U) [DiscreteTopology A] (h : Set.InjOn (⇑ψ) U) : (H.inducedMeasure μA μC) U ≤ μC Set.univ * μA {1}

If φ : A →* B and ψ : B →* C define a short exact sequence of topological groups, and if ψ is injective on an open set U, then the induced measure on U is bounded above by μC Set.univ * μA {1} (possibly infinite).

theorem TopologicalAddGroup.IsSES.inducedMeasure_lt_of_injOn {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C} (H : IsSES φ ψ) [IsTopologicalAddGroup A] [IsTopologicalAddGroup B] [MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure] [IsTopologicalAddGroup C] [LocallyCompactSpace B] [MeasurableSpace C] [BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [T2Space B] [MeasurableSpace B] [BorelSpace B] {U : Set B} (hU : IsOpen U) [DiscreteTopology A] (h : Set.InjOn (⇑ψ) U) : (H.inducedMeasure μA μC) U ≤ μC Set.univ * μA {0}

If φ : A →+ B and ψ : B →+ C define a short exact sequence of additive topological groups, and if ψ is injective on an open set U, then the induced measure on U is bounded above by μC Set.univ * μA {1} (possibly infinite).