Measures on Groups

We develop some properties of measures on (topological) groups

• We define properties on measures: measures that are left or right invariant w.r.t. multiplication.
• We define the measure μ.inv : A ↦ μ(A⁻¹) and show that it is right invariant iff μ is left invariant.
• We define a class IsHaarMeasure μ, requiring that the measure μ is left-invariant, finite on compact sets, and positive on open sets.

We also give analogues of all these notions in the additive world.

class MeasureTheory.Measure.IsAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) : Prop

• map_add_left_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => g + x) μ = μ

A measure μ on a measurable additive group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

class MeasureTheory.Measure.IsMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) : Prop

• map_mul_left_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ

A measure μ on a measurable group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

class MeasureTheory.Measure.IsAddRightInvariant {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) : Prop

• map_add_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => x + g) μ = μ

A measure μ on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

class MeasureTheory.Measure.IsMulRightInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) : Prop

• map_mul_right_eq_self : ∀ (g : G), MeasureTheory.Measure.map (fun x => x * g) μ = μ

A measure μ on a measurable group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

theorem MeasureTheory.map_add_left_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => g + x) μ = μ

theorem MeasureTheory.map_mul_left_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => g * x) μ = μ

theorem MeasureTheory.map_add_right_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => x + g) μ = μ

theorem MeasureTheory.map_mul_right_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => x * g) μ = μ

theorem MeasureTheory.isAddLeftInvariant_smul.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsAddLeftInvariant (c • μ)

instance MeasureTheory.isAddLeftInvariant_smul {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsAddLeftInvariant (c • μ)

Equations

• @MeasureTheory.isAddLeftInvariant_smul = @MeasureTheory.isAddLeftInvariant_smul.proof_1

instance MeasureTheory.isMulLeftInvariant_smul {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsMulLeftInvariant (c • μ)

Equations

• @MeasureTheory.isMulLeftInvariant_smul = @MeasureTheory.isMulLeftInvariant_smul.proof_1

theorem MeasureTheory.isAddRightInvariant_smul.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsAddRightInvariant (c • μ)

instance MeasureTheory.isAddRightInvariant_smul {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsAddRightInvariant (c • μ)

Equations

• @MeasureTheory.isAddRightInvariant_smul = @MeasureTheory.isAddRightInvariant_smul.proof_1

instance MeasureTheory.isMulRightInvariant_smul {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulRightInvariant μ] (c : ENNReal) : MeasureTheory.Measure.IsMulRightInvariant (c • μ)

Equations

• @MeasureTheory.isMulRightInvariant_smul = @MeasureTheory.isMulRightInvariant_smul.proof_1

instance MeasureTheory.isAddLeftInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsAddLeftInvariant (c • μ)

Equations

• @MeasureTheory.isAddLeftInvariant_smul_nnreal = @MeasureTheory.isAddLeftInvariant_smul_nnreal.proof_1

theorem MeasureTheory.isAddLeftInvariant_smul_nnreal.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsAddLeftInvariant (↑c • μ)

instance MeasureTheory.isMulLeftInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsMulLeftInvariant (c • μ)

Equations

• @MeasureTheory.isMulLeftInvariant_smul_nnreal = @MeasureTheory.isMulLeftInvariant_smul_nnreal.proof_1

instance MeasureTheory.isAddRightInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsAddRightInvariant (c • μ)

Equations

• @MeasureTheory.isAddRightInvariant_smul_nnreal = @MeasureTheory.isAddRightInvariant_smul_nnreal.proof_1

theorem MeasureTheory.isAddRightInvariant_smul_nnreal.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsAddRightInvariant (↑c • μ)

instance MeasureTheory.isMulRightInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulRightInvariant μ] (c : NNReal) : MeasureTheory.Measure.IsMulRightInvariant (c • μ)

Equations

• @MeasureTheory.isMulRightInvariant_smul_nnreal = @MeasureTheory.isMulRightInvariant_smul_nnreal.proof_1

theorem MeasureTheory.measurePreserving_add_left {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => g + x

theorem MeasureTheory.measurePreserving_mul_left {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => g * x

theorem MeasureTheory.MeasurePreserving.add_left {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => g + f x

theorem MeasureTheory.MeasurePreserving.mul_left {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => g * f x

theorem MeasureTheory.measurePreserving_add_right {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => x + g

theorem MeasureTheory.measurePreserving_mul_right {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => x * g

theorem MeasureTheory.MeasurePreserving.add_right {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => f x + g

theorem MeasureTheory.MeasurePreserving.mul_right {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G} (hf : MeasureTheory.MeasurePreserving f) : MeasureTheory.MeasurePreserving fun x => f x * g

theorem MeasureTheory.IsMulLeftInvariant.vaddInvariantMeasure.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.VAddInvariantMeasure G G μ

instance MeasureTheory.IsMulLeftInvariant.vaddInvariantMeasure {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.VAddInvariantMeasure G G μ

Equations

• @MeasureTheory.IsMulLeftInvariant.vaddInvariantMeasure = @MeasureTheory.IsMulLeftInvariant.vaddInvariantMeasure.proof_1

instance MeasureTheory.IsMulLeftInvariant.smulInvariantMeasure {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [MeasureTheory.Measure.IsMulLeftInvariant μ] : MeasureTheory.SMulInvariantMeasure G G μ

Equations

• @MeasureTheory.IsMulLeftInvariant.smulInvariantMeasure = @MeasureTheory.IsMulLeftInvariant.smulInvariantMeasure.proof_1

instance MeasureTheory.IsMulRightInvariant.toVAddInvariantMeasure_op {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddRightInvariant μ] : MeasureTheory.VAddInvariantMeasure Gᵃᵒᵖ G μ

Equations

• @MeasureTheory.IsMulRightInvariant.toVAddInvariantMeasure_op = @MeasureTheory.IsMulRightInvariant.toVAddInvariantMeasure_op.proof_1

theorem MeasureTheory.IsMulRightInvariant.toVAddInvariantMeasure_op.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddRightInvariant μ] : MeasureTheory.VAddInvariantMeasure Gᵃᵒᵖ G μ

instance MeasureTheory.IsMulRightInvariant.toSMulInvariantMeasure_op {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [MeasureTheory.Measure.IsMulRightInvariant μ] : MeasureTheory.SMulInvariantMeasure Gᵐᵒᵖ G μ

Equations

• @MeasureTheory.IsMulRightInvariant.toSMulInvariantMeasure_op = @MeasureTheory.IsMulRightInvariant.toSMulInvariantMeasure_op.proof_1

theorem MeasureTheory.Subgroup.vaddInvariantMeasure.proof_1 {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (H : AddSubgroup G) : MeasureTheory.VAddInvariantMeasure { x // x ∈ H } α μ

instance MeasureTheory.Subgroup.vaddInvariantMeasure {G : Type u_4} {α : Type u_5} [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (H : AddSubgroup G) : MeasureTheory.VAddInvariantMeasure { x // x ∈ H } α μ

Equations

• @MeasureTheory.Subgroup.vaddInvariantMeasure = @MeasureTheory.Subgroup.vaddInvariantMeasure.proof_1

instance MeasureTheory.Subgroup.smulInvariantMeasure {G : Type u_4} {α : Type u_5} [Group G] [MulAction G α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (H : Subgroup G) : MeasureTheory.SMulInvariantMeasure { x // x ∈ H } α μ

Equations

• @MeasureTheory.Subgroup.smulInvariantMeasure = @MeasureTheory.Subgroup.smulInvariantMeasure.proof_1

theorem MeasureTheory.forall_measure_preimage_add_iff {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) : (∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => g + h) ⁻¹' A) = ↑↑μ A) ↔ MeasureTheory.Measure.IsAddLeftInvariant μ

An alternative way to prove that μ is left invariant under addition.

theorem MeasureTheory.forall_measure_preimage_mul_iff {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) : (∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => g * h) ⁻¹' A) = ↑↑μ A) ↔ MeasureTheory.Measure.IsMulLeftInvariant μ

An alternative way to prove that μ is left invariant under multiplication.

theorem MeasureTheory.forall_measure_preimage_add_right_iff {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) : (∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => h + g) ⁻¹' A) = ↑↑μ A) ↔ MeasureTheory.Measure.IsAddRightInvariant μ

An alternative way to prove that μ is right invariant under addition.

theorem MeasureTheory.forall_measure_preimage_mul_right_iff {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) : (∀ (g : G) (A : Set G), MeasurableSet A → ↑↑μ ((fun h => h * g) ⁻¹' A) = ↑↑μ A) ↔ MeasureTheory.Measure.IsMulRightInvariant μ

An alternative way to prove that μ is right invariant under multiplication.

instance MeasureTheory.Measure.prod.instIsAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_4} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [MeasureTheory.Measure.IsAddLeftInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsAddLeftInvariant = @MeasureTheory.Measure.prod.instIsAddLeftInvariant.proof_1

theorem MeasureTheory.Measure.prod.instIsAddLeftInvariant.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_2} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [MeasureTheory.Measure.IsAddLeftInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.prod μ ν)

instance MeasureTheory.Measure.prod.instIsMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_4} [Mul H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableMul H] [MeasureTheory.Measure.IsMulLeftInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsMulLeftInvariant = @MeasureTheory.Measure.prod.instIsMulLeftInvariant.proof_1

theorem MeasureTheory.Measure.prod.instIsAddRightInvariant.proof_1 {G : Type u_1} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_2} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [MeasureTheory.Measure.IsAddRightInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.prod μ ν)

instance MeasureTheory.Measure.prod.instIsAddRightInvariant {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [MeasureTheory.Measure.IsAddRightInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_4} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [MeasureTheory.Measure.IsAddRightInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsAddRightInvariant = @MeasureTheory.Measure.prod.instIsAddRightInvariant.proof_1

instance MeasureTheory.Measure.prod.instIsMulRightInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [MeasureTheory.Measure.IsMulRightInvariant μ] [MeasureTheory.SigmaFinite μ] {H : Type u_4} [Mul H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableMul H] [MeasureTheory.Measure.IsMulRightInvariant ν] [MeasureTheory.SigmaFinite ν] : MeasureTheory.Measure.IsMulRightInvariant (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsMulRightInvariant = @MeasureTheory.Measure.prod.instIsMulRightInvariant.proof_1

theorem MeasureTheory.isAddLeftInvariant_map {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] {H : Type u_4} [MeasurableSpace H] [Add H] [MeasurableAdd H] [MeasureTheory.Measure.IsAddLeftInvariant μ] (f : AddHom G H) (hf : Measurable ↑f) (h_surj : Function.Surjective ↑f) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.map (↑f) μ)

theorem MeasureTheory.isMulLeftInvariant_map {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] {H : Type u_4} [MeasurableSpace H] [Mul H] [MeasurableMul H] [MeasureTheory.Measure.IsMulLeftInvariant μ] (f : G →ₙ* H) (hf : Measurable ↑f) (h_surj : Function.Surjective ↑f) : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.map (↑f) μ)

theorem MeasureTheory.isAddLeftInvariant_map_vadd {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} {α : Type u_4} [VAdd α G] [VAddCommClass α G G] [MeasurableSpace α] [MeasurableVAdd α G] [MeasureTheory.Measure.IsAddLeftInvariant μ] (a : α) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ)

The image of a left invariant measure under a left additive action is left invariant, assuming that the action preserves addition.

theorem MeasureTheory.isMulLeftInvariant_map_smul {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} {α : Type u_4} [SMul α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [MeasureTheory.Measure.IsMulLeftInvariant μ] (a : α) : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.map (fun x => a • x) μ)

The image of a left invariant measure under a left action is left invariant, assuming that the action preserves multiplication.

theorem MeasureTheory.isAddRightInvariant_map_vadd {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} {α : Type u_4} [VAdd α G] [VAddCommClass α Gᵃᵒᵖ G] [MeasurableSpace α] [MeasurableVAdd α G] [MeasureTheory.Measure.IsAddRightInvariant μ] (a : α) : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ)

The image of a right invariant measure under a left additive action is right invariant, assuming that the action preserves addition.

theorem MeasureTheory.isMulRightInvariant_map_smul {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} {α : Type u_4} [SMul α G] [SMulCommClass α Gᵐᵒᵖ G] [MeasurableSpace α] [MeasurableSMul α G] [MeasureTheory.Measure.IsMulRightInvariant μ] (a : α) : MeasureTheory.Measure.IsMulRightInvariant (MeasureTheory.Measure.map (fun x => a • x) μ)

The image of a right invariant measure under a left action is right invariant, assuming that the action preserves multiplication.

theorem MeasureTheory.isMulLeftInvariant_map_add_right.proof_1 {G : Type u_1} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.map (fun x => AddOpposite.op g +ᵥ x) μ)

instance MeasureTheory.isMulLeftInvariant_map_add_right {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.map (fun x => x + g) μ)

The image of a left invariant measure under right addition is left invariant.

Equations

• @MeasureTheory.isMulLeftInvariant_map_add_right = @MeasureTheory.isMulLeftInvariant_map_add_right.proof_1

instance MeasureTheory.isMulLeftInvariant_map_mul_right {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.map (fun x => x * g) μ)

The image of a left invariant measure under right multiplication is left invariant.

Equations

• @MeasureTheory.isMulLeftInvariant_map_mul_right = @MeasureTheory.isMulLeftInvariant_map_mul_right.proof_1

instance MeasureTheory.isMulRightInvariant_map_add_left {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.map (fun x => g + x) μ)

The image of a right invariant measure under left addition is right invariant.

Equations

• @MeasureTheory.isMulRightInvariant_map_add_left = @MeasureTheory.isMulRightInvariant_map_add_left.proof_1

theorem MeasureTheory.isMulRightInvariant_map_add_left.proof_1 {G : Type u_1} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.map (fun x => g +ᵥ x) μ)

instance MeasureTheory.isMulRightInvariant_map_mul_left {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) : MeasureTheory.Measure.IsMulRightInvariant (MeasureTheory.Measure.map (fun x => g * x) μ)

The image of a right invariant measure under left multiplication is right invariant.

Equations

• @MeasureTheory.isMulRightInvariant_map_mul_left = @MeasureTheory.isMulRightInvariant_map_mul_left.proof_1

theorem MeasureTheory.map_sub_right_eq_self {G : Type u_2} [MeasurableSpace G] [SubNegMonoid G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => x - g) μ = μ

theorem MeasureTheory.map_div_right_eq_self {G : Type u_2} [MeasurableSpace G] [DivInvMonoid G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) : MeasureTheory.Measure.map (fun x => x / g) μ = μ

theorem MeasureTheory.measurePreserving_sub_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => x - g

theorem MeasureTheory.measurePreserving_div_right {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun x => x / g

@[simp]

theorem MeasureTheory.measure_preimage_add {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) (A : Set G) : ↑↑μ ((fun h => g + h) ⁻¹' A) = ↑↑μ A

We shorten this from measure_preimage_add_left, since left invariant is the preferred option for measures in this formalization.

@[simp]

theorem MeasureTheory.measure_preimage_mul {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) (A : Set G) : ↑↑μ ((fun h => g * h) ⁻¹' A) = ↑↑μ A

We shorten this from measure_preimage_mul_left, since left invariant is the preferred option for measures in this formalization.

@[simp]

theorem MeasureTheory.measure_preimage_add_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (g : G) (A : Set G) : ↑↑μ ((fun h => h + g) ⁻¹' A) = ↑↑μ A

@[simp]

theorem MeasureTheory.measure_preimage_mul_right {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (g : G) (A : Set G) : ↑↑μ ((fun h => h * g) ⁻¹' A) = ↑↑μ A

theorem MeasureTheory.map_add_left_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (x : G) : Filter.map (fun h => x + h) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.map_mul_left_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (x : G) : Filter.map (fun h => x * h) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.map_add_right_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (x : G) : Filter.map (fun h => h + x) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.map_mul_right_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (x : G) : Filter.map (fun h => h * x) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.map_sub_right_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (x : G) : Filter.map (fun t => t - x) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.map_div_right_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (x : G) : Filter.map (fun t => t / x) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.eventually_add_left_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (t + x)) ↔ ∀ᵐ (x : G) ∂μ, p x

theorem MeasureTheory.eventually_mul_left_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x

theorem MeasureTheory.eventually_add_right_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (x + t)) ↔ ∀ᵐ (x : G) ∂μ, p x

theorem MeasureTheory.eventually_mul_right_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x

theorem MeasureTheory.eventually_sub_right_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddRightInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (x - t)) ↔ ∀ᵐ (x : G) ∂μ, p x

theorem MeasureTheory.eventually_div_right_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulRightInvariant μ] (t : G) {p : G → Prop} : (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x

noncomputable def MeasureTheory.Measure.neg {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) : MeasureTheory.Measure G

The measure A ↦ μ (- A), where - A is the pointwise negation of A.

Equations

• MeasureTheory.Measure.neg μ = MeasureTheory.Measure.map Neg.neg μ

noncomputable def MeasureTheory.Measure.inv {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) : MeasureTheory.Measure G

The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

Equations

• MeasureTheory.Measure.inv μ = MeasureTheory.Measure.map Inv.inv μ

class MeasureTheory.Measure.IsNegInvariant {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) : Prop

• neg_eq_self : MeasureTheory.Measure.neg μ = μ

A measure is invariant under negation if - μ = μ. Equivalently, this means that for all measurable A we have μ (- A) = μ A, where - A is the pointwise negation of A.

class MeasureTheory.Measure.IsInvInvariant {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) : Prop

• inv_eq_self : MeasureTheory.Measure.inv μ = μ

A measure is invariant under inversion if μ⁻¹ = μ. Equivalently, this means that for all measurable A we have μ (A⁻¹) = μ A, where A⁻¹ is the pointwise inverse of A.

@[simp]

theorem MeasureTheory.Measure.neg_eq_self {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] : MeasureTheory.Measure.neg μ = μ

@[simp]

theorem MeasureTheory.Measure.inv_eq_self {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] : MeasureTheory.Measure.inv μ = μ

@[simp]

theorem MeasureTheory.Measure.map_neg_eq_self {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] : MeasureTheory.Measure.map Neg.neg μ = μ

@[simp]

theorem MeasureTheory.Measure.map_inv_eq_self {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] : MeasureTheory.Measure.map Inv.inv μ = μ

theorem MeasureTheory.Measure.measurePreserving_neg {G : Type u_2} [MeasurableSpace G] [Neg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] : MeasureTheory.MeasurePreserving Neg.neg

theorem MeasureTheory.Measure.measurePreserving_inv {G : Type u_2} [MeasurableSpace G] [Inv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] : MeasureTheory.MeasurePreserving Inv.inv

@[simp]

theorem MeasureTheory.Measure.neg_apply {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) (s : Set G) : ↑↑(MeasureTheory.Measure.neg μ) s = ↑↑μ (-s)

@[simp]

theorem MeasureTheory.Measure.inv_apply {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) (s : Set G) : ↑↑(MeasureTheory.Measure.inv μ) s = ↑↑μ s⁻¹

@[simp]

theorem MeasureTheory.Measure.neg_neg {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) : MeasureTheory.Measure.neg (MeasureTheory.Measure.neg μ) = μ

@[simp]

theorem MeasureTheory.Measure.inv_inv {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) : MeasureTheory.Measure.inv (MeasureTheory.Measure.inv μ) = μ

@[simp]

theorem MeasureTheory.Measure.measure_neg {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] (A : Set G) : ↑↑μ (-A) = ↑↑μ A

@[simp]

theorem MeasureTheory.Measure.measure_inv {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] (A : Set G) : ↑↑μ A⁻¹ = ↑↑μ A

theorem MeasureTheory.Measure.measure_preimage_neg {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] (A : Set G) : ↑↑μ (Neg.neg ⁻¹' A) = ↑↑μ A

theorem MeasureTheory.Measure.measure_preimage_inv {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] (A : Set G) : ↑↑μ (Inv.inv ⁻¹' A) = ↑↑μ A

instance MeasureTheory.Measure.neg.instSigmaFinite {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.neg μ)

Equations

• @MeasureTheory.Measure.neg.instSigmaFinite = @MeasureTheory.Measure.neg.instSigmaFinite.proof_1

theorem MeasureTheory.Measure.neg.instSigmaFinite.proof_1 {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.map (↑(MeasurableEquiv.neg G)) μ)

instance MeasureTheory.Measure.inv.instSigmaFinite {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ] : MeasureTheory.SigmaFinite (MeasureTheory.Measure.inv μ)

Equations

• @MeasureTheory.Measure.inv.instSigmaFinite = @MeasureTheory.Measure.inv.instSigmaFinite.proof_1

theorem MeasureTheory.Measure.neg.instIsAddRightInvariant.proof_1 {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.neg μ)

instance MeasureTheory.Measure.neg.instIsAddRightInvariant {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.neg μ)

Equations

• @MeasureTheory.Measure.neg.instIsAddRightInvariant = @MeasureTheory.Measure.neg.instIsAddRightInvariant.proof_1

instance MeasureTheory.Measure.inv.instIsMulRightInvariant {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] : MeasureTheory.Measure.IsMulRightInvariant (MeasureTheory.Measure.inv μ)

Equations

• @MeasureTheory.Measure.inv.instIsMulRightInvariant = @MeasureTheory.Measure.inv.instIsMulRightInvariant.proof_1

theorem MeasureTheory.Measure.neg.instIsAddLeftInvariant.proof_1 {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.neg μ)

instance MeasureTheory.Measure.neg.instIsAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddRightInvariant μ] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.neg μ)

Equations

• @MeasureTheory.Measure.neg.instIsAddLeftInvariant = @MeasureTheory.Measure.neg.instIsAddLeftInvariant.proof_1

instance MeasureTheory.Measure.inv.instIsMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulRightInvariant μ] : MeasureTheory.Measure.IsMulLeftInvariant (MeasureTheory.Measure.inv μ)

Equations

• @MeasureTheory.Measure.inv.instIsMulLeftInvariant = @MeasureTheory.Measure.inv.instIsMulLeftInvariant.proof_1

theorem MeasureTheory.Measure.measurePreserving_sub_left {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun t => g - t

theorem MeasureTheory.Measure.measurePreserving_div_left {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun t => g / t

theorem MeasureTheory.Measure.map_sub_left_eq_self {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun t => g - t) μ = μ

theorem MeasureTheory.Measure.map_div_left_eq_self {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun t => g / t) μ = μ

theorem MeasureTheory.Measure.measurePreserving_add_right_neg {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun t => -(g + t)

theorem MeasureTheory.Measure.measurePreserving_mul_right_inv {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.MeasurePreserving fun t => (g * t)⁻¹

theorem MeasureTheory.Measure.map_add_right_neg_eq_self {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsNegInvariant μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun t => -(g + t)) μ = μ

theorem MeasureTheory.Measure.map_mul_right_inv_eq_self {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsInvInvariant μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] (g : G) : MeasureTheory.Measure.map (fun t => (g * t)⁻¹) μ = μ

theorem MeasureTheory.Measure.map_sub_left_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.IsNegInvariant μ] (x : G) : Filter.map (fun t => x - t) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.Measure.map_div_left_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.IsInvInvariant μ] (x : G) : Filter.map (fun t => x / t) (MeasureTheory.Measure.ae μ) = MeasureTheory.Measure.ae μ

theorem MeasureTheory.Measure.Regular.neg.proof_1 {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [ContinuousNeg G] [T2Space G] [MeasureTheory.Measure.Regular μ] : MeasureTheory.Measure.Regular (MeasureTheory.Measure.map (↑(Homeomorph.neg G)) μ)

instance MeasureTheory.Measure.Regular.neg {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [ContinuousNeg G] [T2Space G] [MeasureTheory.Measure.Regular μ] : MeasureTheory.Measure.Regular (MeasureTheory.Measure.neg μ)

Equations

• @MeasureTheory.Measure.Regular.neg = @MeasureTheory.Measure.Regular.neg.proof_1

instance MeasureTheory.Measure.Regular.inv {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [ContinuousInv G] [T2Space G] [MeasureTheory.Measure.Regular μ] : MeasureTheory.Measure.Regular (MeasureTheory.Measure.inv μ)

Equations

• @MeasureTheory.Measure.Regular.inv = @MeasureTheory.Measure.Regular.inv.proof_1

theorem MeasureTheory.regular_neg_iff {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [T2Space G] : MeasureTheory.Measure.Regular (MeasureTheory.Measure.neg μ) ↔ MeasureTheory.Measure.Regular μ

theorem MeasureTheory.regular_inv_iff {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [T2Space G] : MeasureTheory.Measure.Regular (MeasureTheory.Measure.inv μ) ↔ MeasureTheory.Measure.Regular μ

theorem MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] (K : Set G) (hK : IsCompact K) (h : ↑↑μ K ≠ 0) : MeasureTheory.Measure.IsOpenPosMeasure μ

If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.

theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] (K : Set G) (hK : IsCompact K) (h : ↑↑μ K ≠ 0) : MeasureTheory.Measure.IsOpenPosMeasure μ

If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.

abbrev MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular.match_1 {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] {μ : MeasureTheory.Measure G} (motive : (∃ K, IsCompact K ∧ ↑↑μ K ≠ 0) → Prop) : (x : ∃ K, IsCompact K ∧ ↑↑μ K ≠ 0) → ((K : Set G) → (hK : IsCompact K) → (h2K : ↑↑μ K ≠ 0) → motive (_ : ∃ K, IsCompact K ∧ ↑↑μ K ≠ 0)) → motive x

Equations

• MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular.match_1 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (h₀ : μ ≠ 0) : MeasureTheory.Measure.IsOpenPosMeasure μ

A nonzero left-invariant regular measure gives positive mass to any open set.

theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (h₀ : μ ≠ 0) : MeasureTheory.Measure.IsOpenPosMeasure μ

A nonzero left-invariant regular measure gives positive mass to any open set.

theorem MeasureTheory.null_iff_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.Regular μ] {s : Set G} (hs : IsOpen s) : ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0

theorem MeasureTheory.null_iff_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.Regular μ] {s : Set G} (hs : IsOpen s) : ↑↑μ s = 0 ↔ s = ∅ ∨ μ = 0

theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (hμ : μ ≠ 0) {s : Set G} (hs : IsOpen s) : ↑↑μ s ≠ 0 ↔ Set.Nonempty s

theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (hμ : μ ≠ 0) {s : Set G} (hs : IsOpen s) : ↑↑μ s ≠ 0 ↔ Set.Nonempty s

theorem MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (h3μ : μ ≠ 0) {s : Set G} (hs : IsOpen s) : 0 < ↑↑μ s ↔ Set.Nonempty s

theorem MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.Measure.Regular μ] (h3μ : μ ≠ 0) {s : Set G} (hs : IsOpen s) : 0 < ↑↑μ s ↔ Set.Nonempty s

theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] (U : Set G) (hU : IsOpen U) (h'U : Set.Nonempty U) (h : ↑↑μ U ≠ ⊤) {K : Set G} (hK : IsCompact K) : ↑↑μ K < ⊤

If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.

theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] (U : Set G) (hU : IsOpen U) (h'U : Set.Nonempty U) (h : ↑↑μ U ≠ ⊤) {K : Set G} (hK : IsCompact K) : ↑↑μ K < ⊤

If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.

theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant' {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [MeasureTheory.Measure.IsAddLeftInvariant μ] {U : Set G} (hU : Set.Nonempty (interior U)) (h : ↑↑μ U ≠ ⊤) {K : Set G} (hK : IsCompact K) : ↑↑μ K < ⊤

If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.

theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant' {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [MeasureTheory.Measure.IsMulLeftInvariant μ] {U : Set G} (hU : Set.Nonempty (interior U)) (h : ↑↑μ U ≠ ⊤) {K : Set G} (hK : IsCompact K) : ↑↑μ K < ⊤

If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.

@[simp]

theorem MeasureTheory.measure_univ_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [AddGroup G] [TopologicalAddGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsOpenPosMeasure μ] [MeasureTheory.Measure.IsAddLeftInvariant μ] : ↑↑μ Set.univ = ⊤

In a noncompact locally compact additive group, a left-invariant measure which is positive on open sets has infinite mass.

@[simp]

theorem MeasureTheory.measure_univ_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [Group G] [TopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsOpenPosMeasure μ] [MeasureTheory.Measure.IsMulLeftInvariant μ] : ↑↑μ Set.univ = ⊤

In a noncompact locally compact group, a left-invariant measure which is positive on open sets has infinite mass.

instance MeasureTheory.IsAddLeftInvariant.isAddRightInvariant {G : Type u_2} [MeasurableSpace G] [AddCommSemigroup G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.Measure.IsAddRightInvariant μ

In an abelian additive group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use IsAddLeftInvariant as the default hypothesis in abelian groups.

Equations

• @MeasureTheory.IsAddLeftInvariant.isAddRightInvariant = @MeasureTheory.IsAddLeftInvariant.isAddRightInvariant.proof_1

theorem MeasureTheory.IsAddLeftInvariant.isAddRightInvariant.proof_1 {G : Type u_1} [MeasurableSpace G] [AddCommSemigroup G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] : MeasureTheory.Measure.IsAddRightInvariant μ

instance MeasureTheory.IsMulLeftInvariant.isMulRightInvariant {G : Type u_2} [MeasurableSpace G] [CommSemigroup G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] : MeasureTheory.Measure.IsMulRightInvariant μ

In an abelian group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use IsMulLeftInvariant as the default hypothesis in abelian groups.

Equations

• @MeasureTheory.IsMulLeftInvariant.isMulRightInvariant = @MeasureTheory.IsMulLeftInvariant.isMulRightInvariant.proof_1

class MeasureTheory.Measure.IsAddHaarMeasure {G : Type u_4} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) extends MeasureTheory.IsFiniteMeasureOnCompacts , MeasureTheory.Measure.IsAddLeftInvariant , MeasureTheory.Measure.IsOpenPosMeasure : Prop

A measure on an additive group is an additive Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

class MeasureTheory.Measure.IsHaarMeasure {G : Type u_4} [Group G] [TopologicalSpace G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) extends MeasureTheory.IsFiniteMeasureOnCompacts , MeasureTheory.Measure.IsMulLeftInvariant , MeasureTheory.Measure.IsOpenPosMeasure : Prop

A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

theorem MeasureTheory.Measure.isLocallyFiniteMeasure_of_isAddHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [WeaklyLocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.IsLocallyFiniteMeasure μ

instance MeasureTheory.Measure.isLocallyFiniteMeasure_of_isAddHaarMeasure {G : Type u_4} [AddGroup G] [MeasurableSpace G] [TopologicalSpace G] [WeaklyLocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.IsLocallyFiniteMeasure μ

Record that an additive Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.

See Note [lower instance priority]

Equations

• @MeasureTheory.Measure.isLocallyFiniteMeasure_of_isAddHaarMeasure = @MeasureTheory.Measure.isLocallyFiniteMeasure_of_isAddHaarMeasure.proof_1

instance MeasureTheory.Measure.isLocallyFiniteMeasure_of_isHaarMeasure {G : Type u_4} [Group G] [MeasurableSpace G] [TopologicalSpace G] [WeaklyLocallyCompactSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] : MeasureTheory.IsLocallyFiniteMeasure μ

Record that a Haar measure on a locally compact space is locally finite. This is needed as the fact that a measure which is finite on compacts is locally finite is not registered as an instance, to avoid an instance loop.

See Note [lower instance priority].

Equations

• @MeasureTheory.Measure.isLocallyFiniteMeasure_of_isHaarMeasure = @MeasureTheory.Measure.isLocallyFiniteMeasure_of_isHaarMeasure.proof_1

@[simp]

theorem MeasureTheory.Measure.addHaar_singleton {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [TopologicalAddGroup G] [BorelSpace G] (g : G) : ↑↑μ {g} = ↑↑μ {0}

@[simp]

theorem MeasureTheory.Measure.haar_singleton {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [TopologicalGroup G] [BorelSpace G] (g : G) : ↑↑μ {g} = ↑↑μ {1}

theorem MeasureTheory.Measure.IsAddHaarMeasure.smul {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] {c : ENNReal} (cpos : c ≠ 0) (ctop : c ≠ ⊤) : MeasureTheory.Measure.IsAddHaarMeasure (c • μ)

theorem MeasureTheory.Measure.IsHaarMeasure.smul {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] {c : ENNReal} (cpos : c ≠ 0) (ctop : c ≠ ⊤) : MeasureTheory.Measure.IsHaarMeasure (c • μ)

theorem MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddLeftInvariant μ] (K : Set G) (hK : IsCompact K) (h'K : Set.Nonempty (interior K)) (h : ↑↑μ K ≠ 0) (h' : ↑↑μ K ≠ ⊤) : MeasureTheory.Measure.IsAddHaarMeasure μ

If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is an additive Haar measure.

theorem MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsMulLeftInvariant μ] (K : Set G) (hK : IsCompact K) (h'K : Set.Nonempty (interior K)) (h : ↑↑μ K ≠ 0) (h' : ↑↑μ K ≠ ⊤) : MeasureTheory.Measure.IsHaarMeasure μ

If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is a Haar measure.

theorem MeasureTheory.Measure.isAddHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [TopologicalAddGroup G] {H : Type u_4} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalAddGroup H] (f : G →+ H) (hf : Continuous ↑f) (h_surj : Function.Surjective ↑f) (h_prop : Filter.Tendsto (↑f) (Filter.cocompact G) (Filter.cocompact H)) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (↑f) μ)

The image of an additive Haar measure under a continuous surjective proper additive group homomorphism is again an additive Haar measure. See also AddEquiv.isAddHaarMeasure_map.

theorem MeasureTheory.Measure.isHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [BorelSpace G] [TopologicalGroup G] {H : Type u_4} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalGroup H] (f : G →* H) (hf : Continuous ↑f) (h_surj : Function.Surjective ↑f) (h_prop : Filter.Tendsto (↑f) (Filter.cocompact G) (Filter.cocompact H)) : MeasureTheory.Measure.IsHaarMeasure (MeasureTheory.Measure.map (↑f) μ)

The image of a Haar measure under a continuous surjective proper group homomorphism is again a Haar measure. See also MulEquiv.isHaarMeasure_map.

theorem MeasureTheory.Measure.isAddHaarMeasure_map_vadd.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] {α : Type u_2} [BorelSpace G] [TopologicalAddGroup G] [T2Space G] [AddGroup α] [AddAction α G] [VAddCommClass α G G] [MeasurableSpace α] [MeasurableVAdd α G] [ContinuousConstVAdd α G] (a : α) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ)

instance MeasureTheory.Measure.isAddHaarMeasure_map_vadd {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] {α : Type u_4} [BorelSpace G] [TopologicalAddGroup G] [T2Space G] [AddGroup α] [AddAction α G] [VAddCommClass α G G] [MeasurableSpace α] [MeasurableVAdd α G] [ContinuousConstVAdd α G] (a : α) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ)

The image of a Haar measure under map of a left additive action is again a Haar measure

Equations

• @MeasureTheory.Measure.isAddHaarMeasure_map_vadd = @MeasureTheory.Measure.isAddHaarMeasure_map_vadd.proof_1

instance MeasureTheory.Measure.isHaarMeasure_map_smul {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] {α : Type u_4} [BorelSpace G] [TopologicalGroup G] [T2Space G] [Group α] [MulAction α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [ContinuousConstSMul α G] (a : α) : MeasureTheory.Measure.IsHaarMeasure (MeasureTheory.Measure.map (fun x => a • x) μ)

The image of a Haar measure under map of a left action is again a Haar measure.

Equations

• @MeasureTheory.Measure.isHaarMeasure_map_smul = @MeasureTheory.Measure.isHaarMeasure_map_smul.proof_1

theorem MeasureTheory.Measure.isHaarMeasure_map_add_right.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [TopologicalAddGroup G] [T2Space G] (g : G) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (fun x => AddOpposite.op g +ᵥ x) μ)

instance MeasureTheory.Measure.isHaarMeasure_map_add_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [TopologicalAddGroup G] [T2Space G] (g : G) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (fun x => x + g) μ)

The image of a Haar measure under right addition is again a Haar measure.

Equations

• @MeasureTheory.Measure.isHaarMeasure_map_add_right = @MeasureTheory.Measure.isHaarMeasure_map_add_right.proof_1

instance MeasureTheory.Measure.isHaarMeasure_map_mul_right {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [BorelSpace G] [TopologicalGroup G] [T2Space G] (g : G) : MeasureTheory.Measure.IsHaarMeasure (MeasureTheory.Measure.map (fun x => x * g) μ)

The image of a Haar measure under right multiplication is again a Haar measure.

Equations

• @MeasureTheory.Measure.isHaarMeasure_map_mul_right = @MeasureTheory.Measure.isHaarMeasure_map_mul_right.proof_1

theorem AddEquiv.isAddHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [BorelSpace G] [TopologicalAddGroup G] {H : Type u_4} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalAddGroup H] (e : G ≃+ H) (he : Continuous ↑e) (hesymm : Continuous ↑(AddEquiv.symm e)) : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (↑e) μ)

A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map.

theorem MulEquiv.isHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [BorelSpace G] [TopologicalGroup G] {H : Type u_4} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalGroup H] (e : G ≃* H) (he : Continuous ↑e) (hesymm : Continuous ↑(MulEquiv.symm e)) : MeasureTheory.Measure.IsHaarMeasure (MeasureTheory.Measure.map (↑e) μ)

A convenience wrapper for MeasureTheory.Measure.isHaarMeasure_map.

theorem ContinuousLinearEquiv.isAddHaarMeasure_map {E : Type u_4} {F : Type u_5} {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module S F] [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F] [T2Space F] [TopologicalAddGroup F] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (L : E ≃SL[σ] F) (μ : MeasureTheory.Measure E) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.map (↑L) μ)

A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`.

theorem MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [SigmaCompactSpace G] : MeasureTheory.SigmaFinite μ

instance MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] [SigmaCompactSpace G] : MeasureTheory.SigmaFinite μ

A Haar measure on a σ-compact space is σ-finite.

See Note [lower instance priority]

Equations

• @MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite = @MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite.proof_1

instance MeasureTheory.Measure.IsHaarMeasure.sigmaFinite {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] [SigmaCompactSpace G] : MeasureTheory.SigmaFinite μ

A Haar measure on a σ-compact space is σ-finite.

See Note [lower instance priority]

Equations

• @MeasureTheory.Measure.IsHaarMeasure.sigmaFinite = @MeasureTheory.Measure.IsHaarMeasure.sigmaFinite.proof_1

theorem MeasureTheory.Measure.prod.instIsAddHaarMeasure.proof_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ∀ {x : MeasurableSpace G} {H : Type u_2} [inst : AddGroup H] [inst_1 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure H) [inst_2 : MeasureTheory.Measure.IsAddHaarMeasure μ] [inst_3 : MeasureTheory.Measure.IsAddHaarMeasure ν] [inst_4 : MeasureTheory.SigmaFinite μ] [inst_5 : MeasureTheory.SigmaFinite ν] [inst_6 : MeasurableAdd G] [inst_7 : MeasurableAdd H], MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.prod μ ν)

instance MeasureTheory.Measure.prod.instIsAddHaarMeasure {G : Type u_4} [AddGroup G] [TopologicalSpace G] : ∀ {x : MeasurableSpace G} {H : Type u_5} [inst : AddGroup H] [inst_1 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure H) [inst_2 : MeasureTheory.Measure.IsAddHaarMeasure μ] [inst_3 : MeasureTheory.Measure.IsAddHaarMeasure ν] [inst_4 : MeasureTheory.SigmaFinite μ] [inst_5 : MeasureTheory.SigmaFinite ν] [inst_6 : MeasurableAdd G] [inst_7 : MeasurableAdd H], MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsAddHaarMeasure = @MeasureTheory.Measure.prod.instIsAddHaarMeasure.proof_1

instance MeasureTheory.Measure.prod.instIsHaarMeasure {G : Type u_4} [Group G] [TopologicalSpace G] : ∀ {x : MeasurableSpace G} {H : Type u_5} [inst : Group H] [inst_1 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure H) [inst_2 : MeasureTheory.Measure.IsHaarMeasure μ] [inst_3 : MeasureTheory.Measure.IsHaarMeasure ν] [inst_4 : MeasureTheory.SigmaFinite μ] [inst_5 : MeasureTheory.SigmaFinite ν] [inst_6 : MeasurableMul G] [inst_7 : MeasurableMul H], MeasureTheory.Measure.IsHaarMeasure (MeasureTheory.Measure.prod μ ν)

Equations

• @MeasureTheory.Measure.prod.instIsHaarMeasure = @MeasureTheory.Measure.prod.instIsHaarMeasure.proof_1

theorem MeasureTheory.Measure.IsAddHaarMeasure.noAtoms.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [Filter.NeBot (nhdsWithin 0 {0}ᶜ)] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.NoAtoms μ

instance MeasureTheory.Measure.IsAddHaarMeasure.noAtoms {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [Filter.NeBot (nhdsWithin 0 {0}ᶜ)] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.NoAtoms μ

If the zero element of an additive group is not isolated, then an additive Haar measure on this group has no atoms.

This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.

Equations

• @MeasureTheory.Measure.IsAddHaarMeasure.noAtoms = @MeasureTheory.Measure.IsAddHaarMeasure.noAtoms.proof_1

instance MeasureTheory.Measure.IsHaarMeasure.noAtoms {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [Filter.NeBot (nhdsWithin 1 {1}ᶜ)] (μ : MeasureTheory.Measure G) [MeasureTheory.Measure.IsHaarMeasure μ] : MeasureTheory.NoAtoms μ

If the neutral element of a group is not isolated, then a Haar measure on this group has no atoms.

The additive version of this instance applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.

Equations

• @MeasureTheory.Measure.IsHaarMeasure.noAtoms = @MeasureTheory.Measure.IsHaarMeasure.noAtoms.proof_1