# 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.

source
theorem MeasureTheory.map_mul_left_eq_self {G : Type u_1} [MeasurableSpace G] [Mul G] (μ : Measure G) [μ.IsMulLeftInvariant] (g : G) :
Measure.map (fun (x : G) => g * x) μ = μ
source
theorem MeasureTheory.map_add_left_eq_self {G : Type u_1} [MeasurableSpace G] [Add G] (μ : Measure G) [μ.IsAddLeftInvariant] (g : G) :
Measure.map (fun (x : G) => g + x) μ = μ
source
theorem MeasureTheory.map_mul_right_eq_self {G : Type u_1} [MeasurableSpace G] [Mul G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) :
Measure.map (fun (x : G) => x * g) μ = μ
source
theorem MeasureTheory.map_add_right_eq_self {G : Type u_1} [MeasurableSpace G] [Add G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) :
Measure.map (fun (x : G) => x + g) μ = μ
source
instance MeasureTheory.isMulLeftInvariant_smul {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [μ.IsMulLeftInvariant] (c : ENNReal) :
(c • μ).IsMulLeftInvariant
source
instance MeasureTheory.isAddLeftInvariant_smul {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [μ.IsAddLeftInvariant] (c : ENNReal) :
(c • μ).IsAddLeftInvariant
source
instance MeasureTheory.isMulRightInvariant_smul {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [μ.IsMulRightInvariant] (c : ENNReal) :
(c • μ).IsMulRightInvariant
source
instance MeasureTheory.isAddRightInvariant_smul {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [μ.IsAddRightInvariant] (c : ENNReal) :
(c • μ).IsAddRightInvariant
source
instance MeasureTheory.isMulLeftInvariant_smul_nnreal {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [μ.IsMulLeftInvariant] (c : NNReal) :
(c • μ).IsMulLeftInvariant
source
instance MeasureTheory.isAddLeftInvariant_smul_nnreal {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [μ.IsAddLeftInvariant] (c : NNReal) :
(c • μ).IsAddLeftInvariant
source
instance MeasureTheory.isMulRightInvariant_smul_nnreal {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [μ.IsMulRightInvariant] (c : NNReal) :
(c • μ).IsMulRightInvariant
source
instance MeasureTheory.isAddRightInvariant_smul_nnreal {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [μ.IsAddRightInvariant] (c : NNReal) :
(c • μ).IsAddRightInvariant
source
theorem MeasureTheory.measurePreserving_mul_left {G : Type u_1} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] (g : G) :
MeasurePreserving (fun (x : G) => g * x) μ μ
source
theorem MeasureTheory.measurePreserving_add_left {G : Type u_1} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddLeftInvariant] (g : G) :
MeasurePreserving (fun (x : G) => g + x) μ μ
source
theorem MeasureTheory.MeasurePreserving.mul_left {G : Type u_1} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] (g : G) {X : Type u_3} [MeasurableSpace X] {μ' : Measure X} {f : X → G} (hf : MeasurePreserving f μ' μ) :
MeasurePreserving (fun (x : X) => g * f x) μ' μ
source
theorem MeasureTheory.MeasurePreserving.add_left {G : Type u_1} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddLeftInvariant] (g : G) {X : Type u_3} [MeasurableSpace X] {μ' : Measure X} {f : X → G} (hf : MeasurePreserving f μ' μ) :
MeasurePreserving (fun (x : X) => g + f x) μ' μ
source
theorem MeasureTheory.measurePreserving_mul_right {G : Type u_1} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) :
MeasurePreserving (fun (x : G) => x * g) μ μ
source
theorem MeasureTheory.measurePreserving_add_right {G : Type u_1} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) :
MeasurePreserving (fun (x : G) => x + g) μ μ
source
theorem MeasureTheory.MeasurePreserving.mul_right {G : Type u_1} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) {X : Type u_3} [MeasurableSpace X] {μ' : Measure X} {f : X → G} (hf : MeasurePreserving f μ' μ) :
MeasurePreserving (fun (x : X) => f x * g) μ' μ
source
theorem MeasureTheory.MeasurePreserving.add_right {G : Type u_1} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) {X : Type u_3} [MeasurableSpace X] {μ' : Measure X} {f : X → G} (hf : MeasurePreserving f μ' μ) :
MeasurePreserving (fun (x : X) => f x + g) μ' μ
source
instance MeasureTheory.Subgroup.smulInvariantMeasure {G : Type u_3} {α : Type u_4} [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α} [SMulInvariantMeasure G α μ] (H : Subgroup G) :
SMulInvariantMeasure (↥H) α μ
source
instance MeasureTheory.Subgroup.vaddInvariantMeasure {G : Type u_3} {α : Type u_4} [AddGroup G] [AddAction G α] [MeasurableSpace α] {μ : Measure α} [VAddInvariantMeasure G α μ] (H : AddSubgroup G) :
VAddInvariantMeasure (↥H) α μ
source
theorem MeasureTheory.forall_measure_preimage_mul_iff {G : Type u_1} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : Measure G) :
(∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun (h : G) => g * h) ⁻¹' A) = μ A) ↔ μ.IsMulLeftInvariant

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

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

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

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

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

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

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

source
instance MeasureTheory.Measure.prod.instIsMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [MeasurableMul G] [μ.IsMulLeftInvariant] [SFinite μ] {H : Type u_3} [Mul H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableMul H] [ν.IsMulLeftInvariant] [SFinite ν] :
(μ.prod ν).IsMulLeftInvariant
source
instance MeasureTheory.Measure.prod.instIsAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [MeasurableAdd G] [μ.IsAddLeftInvariant] [SFinite μ] {H : Type u_3} [Add H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableAdd H] [ν.IsAddLeftInvariant] [SFinite ν] :
(μ.prod ν).IsAddLeftInvariant
source
instance MeasureTheory.Measure.prod.instIsMulRightInvariant {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [MeasurableMul G] [μ.IsMulRightInvariant] [SFinite μ] {H : Type u_3} [Mul H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableMul H] [ν.IsMulRightInvariant] [SFinite ν] :
(μ.prod ν).IsMulRightInvariant
source
instance MeasureTheory.Measure.prod.instIsAddRightInvariant {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [MeasurableAdd G] [μ.IsAddRightInvariant] [SFinite μ] {H : Type u_3} [Add H] {mH : MeasurableSpace H} {ν : Measure H} [MeasurableAdd H] [ν.IsAddRightInvariant] [SFinite ν] :
(μ.prod ν).IsAddRightInvariant
source
theorem MeasureTheory.isMulLeftInvariant_map {G : Type u_1} [MeasurableSpace G] [Mul G] {μ : Measure G} [MeasurableMul G] {H : Type u_3} [MeasurableSpace H] [Mul H] [MeasurableMul H] [μ.IsMulLeftInvariant] (f : G →ₙ* H) (hf : Measurable ⇑f) (h_surj : Function.Surjective ⇑f) :
(Measure.map (⇑f) μ).IsMulLeftInvariant
source
theorem MeasureTheory.isAddLeftInvariant_map {G : Type u_1} [MeasurableSpace G] [Add G] {μ : Measure G} [MeasurableAdd G] {H : Type u_3} [MeasurableSpace H] [Add H] [MeasurableAdd H] [μ.IsAddLeftInvariant] (f : G →ₙ+ H) (hf : Measurable ⇑f) (h_surj : Function.Surjective ⇑f) :
(Measure.map (⇑f) μ).IsAddLeftInvariant
source
theorem MeasureTheory.isMulLeftInvariant_map_smul {G : Type u_1} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : Measure G} {α : Type u_3} [SMul α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [μ.IsMulLeftInvariant] (a : α) :
(Measure.map (fun (x : G) => a • x) μ).IsMulLeftInvariant

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
theorem MeasureTheory.map_div_right_eq_self {G : Type u_1} [MeasurableSpace G] [DivInvMonoid G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) :
Measure.map (fun (x : G) => x / g) μ = μ
source
theorem MeasureTheory.map_sub_right_eq_self {G : Type u_1} [MeasurableSpace G] [SubNegMonoid G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) :
Measure.map (fun (x : G) => x - g) μ = μ
source
theorem MeasureTheory.measurePreserving_div_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) :
MeasurePreserving (fun (x : G) => x / g) μ μ
source
theorem MeasureTheory.measurePreserving_sub_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) :
MeasurePreserving (fun (x : G) => x - g) μ μ
source
@[simp]
theorem MeasureTheory.measure_preimage_mul {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] (g : G) (A : Set G) :
μ ((fun (h : G) => g * h) ⁻¹' A) = μ A

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

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

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

source
@[simp]
theorem MeasureTheory.measure_preimage_mul_right {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (g : G) (A : Set G) :
μ ((fun (h : G) => h * g) ⁻¹' A) = μ A
source
@[simp]
theorem MeasureTheory.measure_preimage_add_right {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (g : G) (A : Set G) :
μ ((fun (h : G) => h + g) ⁻¹' A) = μ A
source
theorem MeasureTheory.map_mul_left_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] (x : G) :
Filter.map (fun (h : G) => x * h) (ae μ) = ae μ
source
theorem MeasureTheory.map_add_left_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddLeftInvariant] (x : G) :
Filter.map (fun (h : G) => x + h) (ae μ) = ae μ
source
theorem MeasureTheory.map_mul_right_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (x : G) :
Filter.map (fun (h : G) => h * x) (ae μ) = ae μ
source
theorem MeasureTheory.map_add_right_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (x : G) :
Filter.map (fun (h : G) => h + x) (ae μ) = ae μ
source
theorem MeasureTheory.map_div_right_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (x : G) :
Filter.map (fun (t : G) => t / x) (ae μ) = ae μ
source
theorem MeasureTheory.map_sub_right_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (x : G) :
Filter.map (fun (t : G) => t - x) (ae μ) = ae μ
source
theorem MeasureTheory.eventually_mul_left_iff {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.eventually_add_left_iff {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddLeftInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (t + x)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.eventually_mul_right_iff {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.eventually_add_right_iff {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (x + t)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.eventually_div_right_iff {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : Measure G) [μ.IsMulRightInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.eventually_sub_right_iff {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddRightInvariant] (t : G) {p : G → Prop} :
(∀ᵐ (x : G) ∂μ, p (x - t)) ↔ ∀ᵐ (x : G) ∂μ, p x
source
theorem MeasureTheory.Subgroup.index_mul_measure {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (H : Subgroup G) [H.FiniteIndex] (hH : MeasurableSet ↑H) (μ : Measure G) [μ.IsMulLeftInvariant] :
↑H.index * μ ↑H = μ Set.univ
source
theorem MeasureTheory.AddSubgroup.index_mul_measure {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (H : AddSubgroup G) [H.FiniteIndex] (hH : MeasurableSet ↑H) (μ : Measure G) [μ.IsAddLeftInvariant] :
↑H.index * μ ↑H = μ Set.univ
source
noncomputable def MeasureTheory.Measure.inv {G : Type u_1} [MeasurableSpace G] [Inv G] (μ : Measure G) :
Measure G

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

Equations

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

Instances For

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

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

Equations

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

Instances For

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

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`.

- neg_eq_self : μ.neg = μ

Instances

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

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`.

- inv_eq_self : μ.inv = μ

Instances

source
theorem MeasureTheory.Measure.inv_def {G : Type u_1} [MeasurableSpace G] [Inv G] (μ : Measure G) :
μ.inv = map Inv.inv μ
source
theorem MeasureTheory.Measure.neg_def {G : Type u_1} [MeasurableSpace G] [Neg G] (μ : Measure G) :
μ.neg = map Neg.neg μ
source
@[simp]
theorem MeasureTheory.Measure.inv_eq_self {G : Type u_1} [MeasurableSpace G] [Inv G] (μ : Measure G) [μ.IsInvInvariant] :
μ.inv = μ
source
@[simp]
theorem MeasureTheory.Measure.neg_eq_self {G : Type u_1} [MeasurableSpace G] [Neg G] (μ : Measure G) [μ.IsNegInvariant] :
μ.neg = μ
source
@[simp]
theorem MeasureTheory.Measure.map_inv_eq_self {G : Type u_1} [MeasurableSpace G] [Inv G] (μ : Measure G) [μ.IsInvInvariant] :
map Inv.inv μ = μ
source
@[simp]
theorem MeasureTheory.Measure.map_neg_eq_self {G : Type u_1} [MeasurableSpace G] [Neg G] (μ : Measure G) [μ.IsNegInvariant] :
map Neg.neg μ = μ
source
theorem MeasureTheory.Measure.measurePreserving_inv {G : Type u_1} [MeasurableSpace G] [Inv G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] :
MeasurePreserving Inv.inv μ μ
source
theorem MeasureTheory.Measure.measurePreserving_neg {G : Type u_1} [MeasurableSpace G] [Neg G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] :
MeasurePreserving Neg.neg μ μ
source
instance MeasureTheory.Measure.inv.instSFinite {G : Type u_1} [MeasurableSpace G] [Inv G] (μ : Measure G) [SFinite μ] :
SFinite μ.inv
source
instance MeasureTheory.Measure.neg.instSFinite {G : Type u_1} [MeasurableSpace G] [Neg G] (μ : Measure G) [SFinite μ] :
SFinite μ.neg
source
@[simp]
theorem MeasureTheory.Measure.inv_apply {G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : Measure G) (s : Set G) :
μ.inv s = μ s⁻¹
source
@[simp]
theorem MeasureTheory.Measure.neg_apply {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : Measure G) (s : Set G) :
μ.neg s = μ (-s)
source
@[simp]
theorem MeasureTheory.Measure.inv_inv {G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : Measure G) :
μ.inv.inv = μ
source
@[simp]
theorem MeasureTheory.Measure.neg_neg {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : Measure G) :
μ.neg.neg = μ
source
@[simp]
theorem MeasureTheory.Measure.measure_inv {G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] (A : Set G) :
μ A⁻¹ = μ A
source
@[simp]
theorem MeasureTheory.Measure.measure_neg {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] (A : Set G) :
μ (-A) = μ A
source
theorem MeasureTheory.Measure.measure_preimage_inv {G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] (A : Set G) :
μ (Inv.inv ⁻¹' A) = μ A
source
theorem MeasureTheory.Measure.measure_preimage_neg {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] (A : Set G) :
μ (Neg.neg ⁻¹' A) = μ A
source
instance MeasureTheory.Measure.inv.instSigmaFinite {G : Type u_1} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : Measure G) [SigmaFinite μ] :
SigmaFinite μ.inv
source
instance MeasureTheory.Measure.neg.instSigmaFinite {G : Type u_1} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : Measure G) [SigmaFinite μ] :
SigmaFinite μ.neg
source
instance MeasureTheory.Measure.inv.instIsMulRightInvariant {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : Measure G} [μ.IsMulLeftInvariant] :
μ.inv.IsMulRightInvariant
source
instance MeasureTheory.Measure.neg.instIsAddRightInvariant {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddLeftInvariant] :
μ.neg.IsAddRightInvariant
source
instance MeasureTheory.Measure.inv.instIsMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : Measure G} [μ.IsMulRightInvariant] :
μ.inv.IsMulLeftInvariant
source
instance MeasureTheory.Measure.neg.instIsAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : Measure G} [μ.IsAddRightInvariant] :
μ.neg.IsAddLeftInvariant
source
theorem MeasureTheory.Measure.measurePreserving_div_left {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
MeasurePreserving (fun (t : G) => g / t) μ μ
source
theorem MeasureTheory.Measure.measurePreserving_sub_left {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
MeasurePreserving (fun (t : G) => g - t) μ μ
source
theorem MeasureTheory.Measure.map_div_left_eq_self {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
map (fun (t : G) => g / t) μ = μ
source
theorem MeasureTheory.Measure.map_sub_left_eq_self {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
map (fun (t : G) => g - t) μ = μ
source
theorem MeasureTheory.Measure.measurePreserving_mul_right_inv {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
MeasurePreserving (fun (t : G) => (g * t)⁻¹) μ μ
source
theorem MeasureTheory.Measure.measurePreserving_add_right_neg {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
MeasurePreserving (fun (t : G) => -(g + t)) μ μ
source
theorem MeasureTheory.Measure.map_mul_right_inv_eq_self {G : Type u_1} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
map (fun (t : G) => (g * t)⁻¹) μ = μ
source
theorem MeasureTheory.Measure.map_add_right_neg_eq_self {G : Type u_1} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
map (fun (t : G) => -(g + t)) μ = μ
source
instance MeasureTheory.Measure.instIsMulLeftInvariantCount {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] :
count.IsMulLeftInvariant
source
instance MeasureTheory.Measure.instIsAddLeftInvariantCount {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] :
count.IsAddLeftInvariant
source
instance MeasureTheory.Measure.instIsMulRightInvariantCount {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] :
count.IsMulRightInvariant
source
instance MeasureTheory.Measure.instIsAddRightInvariantCount {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] :
count.IsAddRightInvariant
source
theorem MeasureTheory.Measure.IsMulLeftInvariant.comap {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] {H : Type u_3} [Group H] {mH : MeasurableSpace H} [MeasurableMul H] (μ : Measure H) [μ.IsMulLeftInvariant] {f : G →* H} (hf : MeasurableEmbedding ⇑f) :
(comap (⇑f) μ).IsMulLeftInvariant
source
theorem MeasureTheory.Measure.IsAddLeftInvariant.comap {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] {H : Type u_3} [AddGroup H] {mH : MeasurableSpace H} [MeasurableAdd H] (μ : Measure H) [μ.IsAddLeftInvariant] {f : G →+ H} (hf : MeasurableEmbedding ⇑f) :
(comap (⇑f) μ).IsAddLeftInvariant
source
theorem MeasureTheory.Measure.IsMulRightInvariant.comap {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] {H : Type u_3} [Group H] {mH : MeasurableSpace H} [MeasurableMul H] (μ : Measure H) [μ.IsMulRightInvariant] {f : G →* H} (hf : MeasurableEmbedding ⇑f) :
(comap (⇑f) μ).IsMulRightInvariant
source
theorem MeasureTheory.Measure.IsAddRightInvariant.comap {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] {H : Type u_3} [AddGroup H] {mH : MeasurableSpace H} [MeasurableAdd H] (μ : Measure H) [μ.IsAddRightInvariant] {f : G →+ H} (hf : MeasurableEmbedding ⇑f) :
(comap (⇑f) μ).IsAddRightInvariant
source
instance MeasureTheory.Measure.instIsInvInvariantCount {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableInv G] :
count.IsInvInvariant
source
instance MeasureTheory.Measure.instIsNegInvariantCount {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableNeg G] :
count.IsNegInvariant
source
theorem MeasureTheory.Measure.map_div_left_ae {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableInv G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] [μ.IsInvInvariant] (x : G) :
Filter.map (fun (t : G) => x / t) (ae μ) = ae μ
source
theorem MeasureTheory.Measure.map_sub_left_ae {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableNeg G] [MeasurableAdd G] (μ : Measure G) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (x : G) :
Filter.map (fun (t : G) => x - t) (ae μ) = ae μ
source
instance MeasureTheory.Measure.IsFiniteMeasureOnCompacts.inv {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [ContinuousInv G] [IsFiniteMeasureOnCompacts μ] :
IsFiniteMeasureOnCompacts μ.inv
source
instance MeasureTheory.Measure.IsFiniteMeasureOnCompacts.neg {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [ContinuousNeg G] [IsFiniteMeasureOnCompacts μ] :
IsFiniteMeasureOnCompacts μ.neg
source
instance MeasureTheory.Measure.IsOpenPosMeasure.inv {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [ContinuousInv G] [μ.IsOpenPosMeasure] :
μ.inv.IsOpenPosMeasure
source
instance MeasureTheory.Measure.IsOpenPosMeasure.neg {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [ContinuousNeg G] [μ.IsOpenPosMeasure] :
μ.neg.IsOpenPosMeasure
source
instance MeasureTheory.Measure.Regular.inv {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [ContinuousInv G] [μ.Regular] :
μ.inv.Regular
source
instance MeasureTheory.Measure.Regular.neg {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [ContinuousNeg G] [μ.Regular] :
μ.neg.Regular
source
instance MeasureTheory.Measure.InnerRegular.inv {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [ContinuousInv G] [μ.InnerRegular] :
μ.inv.InnerRegular
source
instance MeasureTheory.Measure.InnerRegular.neg {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [ContinuousNeg G] [μ.InnerRegular] :
μ.neg.InnerRegular
source
instance MeasureTheory.innerRegular_map_smul {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} {α : Type u_3} [Monoid α] [MulAction α G] [ContinuousConstSMul α G] [μ.InnerRegular] (a : α) :
(Measure.map (fun (x : G) => a • x) μ).InnerRegular

The image of an inner regular measure under map of a left action is again inner regular.

source
instance MeasureTheory.innerRegular_map_vadd {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} {α : Type u_3} [AddMonoid α] [AddAction α G] [ContinuousConstVAdd α G] [μ.InnerRegular] (a : α) :
(Measure.map (fun (x : G) => a +ᵥ x) μ).InnerRegular

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

source
instance MeasureTheory.innerRegular_map_mul_left {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.InnerRegular] (g : G) :
(Measure.map (fun (x : G) => g * x) μ).InnerRegular

The image of an inner regular measure under left multiplication is again inner regular.

source
instance MeasureTheory.innerRegular_map_add_left {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.InnerRegular] (g : G) :
(Measure.map (fun (x : G) => g + x) μ).InnerRegular

The image of an inner regular measure under left addition is again inner regular.

source
instance MeasureTheory.innerRegular_map_mul_right {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.InnerRegular] (g : G) :
(Measure.map (fun (x : G) => x * g) μ).InnerRegular

The image of an inner regular measure under right multiplication is again inner regular.

source
instance MeasureTheory.innerRegular_map_add_right {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.InnerRegular] (g : G) :
(Measure.map (fun (x : G) => x + g) μ).InnerRegular

The image of an inner regular measure under right addition is again inner regular.

source
theorem MeasureTheory.regular_inv_iff {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] :
μ.inv.Regular ↔ μ.Regular
source
theorem MeasureTheory.regular_neg_iff {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] :
μ.neg.Regular ↔ μ.Regular
source
theorem MeasureTheory.innerRegular_inv_iff {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] :
μ.inv.InnerRegular ↔ μ.InnerRegular
source
theorem MeasureTheory.innerRegular_neg_iff {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] :
μ.neg.InnerRegular ↔ μ.InnerRegular
source
theorem MeasureTheory.eventually_nhds_one_measure_smul_diff_lt {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε ≠ 0) :
∀ᶠ (g : G) in nhds 1, μ (g • k \ k) < ε

Continuity of the measure of translates of a compact set: Given a compact set `k` in a topological group, for `g` close enough to the origin, `μ (g • k \ k)` is arbitrarily small.

source
theorem MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε ≠ 0) :
∀ᶠ (g : G) in nhds 0, μ ((g +ᵥ k) \ k) < ε
source
theorem MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) :
Filter.Tendsto (fun (g : G) => μ (g • k \ k)) (nhds 1) (nhds 0)

Continuity of the measure of translates of a compact set: Given a closed compact set `k` in a topological group, the measure of `g • k \ k` tends to zero as `g` tends to `1`.

source
theorem MeasureTheory.tendsto_measure_vadd_diff_isCompact_isClosed {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) :
Filter.Tendsto (fun (g : G) => μ ((g +ᵥ k) \ k)) (nhds 0) (nhds 0)
source
theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] (K : Set G) (hK : IsCompact K) (h : μ K ≠ 0) :
μ.IsOpenPosMeasure

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

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

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

source
@[instance 80]
instance MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] [NeZero μ] :
μ.IsOpenPosMeasure

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

source
@[instance 80]
instance MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] [NeZero μ] :
μ.IsOpenPosMeasure

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

source
@[instance 80]
instance MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.InnerRegular] [NeZero μ] :
μ.IsOpenPosMeasure

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

source
@[instance 80]
instance MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.InnerRegular] [NeZero μ] :
μ.IsOpenPosMeasure

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

source
theorem MeasureTheory.null_iff_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] {s : Set G} (hs : IsOpen s) :
μ s = 0 ↔ s = ∅ ∨ μ = 0
source
theorem MeasureTheory.null_iff_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] {s : Set G} (hs : IsOpen s) :
μ s = 0 ↔ s = ∅ ∨ μ = 0
source
theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] (hμ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
μ s ≠ 0 ↔ s.Nonempty
source
theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] (hμ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
μ s ≠ 0 ↔ s.Nonempty
source
theorem MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] (h3μ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
0 < μ s ↔ s.Nonempty
source
theorem MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] (h3μ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
0 < μ s ↔ s.Nonempty
source
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] (U : Set G) (hU : IsOpen U) (h'U : U.Nonempty) (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.

source
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] (U : Set G) (hU : IsOpen U) (h'U : U.Nonempty) (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.

source
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant' {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] {U : Set G} (hU : (interior U).Nonempty) (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.

source
theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant' {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] {U : Set G} (hU : (interior U).Nonempty) (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.

source
@[simp]
theorem MeasureTheory.measure_univ_of_isMulLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [Group G] [IsTopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : Measure G) [μ.IsOpenPosMeasure] [μ.IsMulLeftInvariant] :
μ Set.univ = ⊤

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

source
@[simp]
theorem MeasureTheory.measure_univ_of_isAddLeftInvariant {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [AddGroup G] [IsTopologicalAddGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : Measure G) [μ.IsOpenPosMeasure] [μ.IsAddLeftInvariant] :
μ Set.univ = ⊤

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

source
theorem MeasurableSet.mul_closure_one_eq {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [Group G] [IsTopologicalGroup G] {s : Set G} (hs : MeasurableSet s) :
s * closure {1} = s
source
theorem MeasurableSet.add_closure_zero_eq {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (hs : MeasurableSet s) :
s + closure {0} = s
source
@[simp]
theorem MeasureTheory.measure_mul_closure_one {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [Group G] [IsTopologicalGroup G] (s : Set G) (μ : Measure G) :
μ (s * closure {1}) = μ s
source
@[simp]
theorem MeasureTheory.measure_add_closure_zero {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : Set G) (μ : Measure G) :
μ (s + closure {0}) = μ s
source
theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [Group G] [IsTopologicalGroup G] [h : μ.InnerRegularCompactLTTop] :
μ.InnerRegularWRT (fun (s : Set G) => IsCompact s ∧ IsClosed s) fun (s : Set G) => MeasurableSet s ∧ μ s ≠ ⊤
source
theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : Measure G} [AddGroup G] [IsTopologicalAddGroup G] [h : μ.InnerRegularCompactLTTop] :
μ.InnerRegularWRT (fun (s : Set G) => IsCompact s ∧ IsClosed s) fun (s : Set G) => MeasurableSet s ∧ μ s ≠ ⊤
source
@[instance 100]
instance MeasureTheory.IsMulLeftInvariant.isMulRightInvariant {G : Type u_1} [MeasurableSpace G] [CommSemigroup G] {μ : Measure G} [μ.IsMulLeftInvariant] :
μ.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.

source
@[instance 100]
instance MeasureTheory.IsAddLeftInvariant.isAddRightInvariant {G : Type u_1} [MeasurableSpace G] [AddCommSemigroup G] {μ : Measure G} [μ.IsAddLeftInvariant] :
μ.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.

source
class MeasureTheory.Measure.IsAddHaarMeasure {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] (μ : Measure G) extends MeasureTheory.IsFiniteMeasureOnCompacts μ, μ.IsAddLeftInvariant, μ.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.

Textbooks generally require an additional regularity assumption to ensure nice behavior on arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or `[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our sense is automatically regular and inner regular on second countable locally compact groups, as checked just below this definition.

- lt_top_of_isCompact ⦃K : Set G⦄ : IsCompact K → μ K < ⊤
- map_add_left_eq_self (g : G) : map (fun (x : G) => g + x) μ = μ
- open_pos (U : Set G) : IsOpen U → U.Nonempty → μ U ≠ 0

Instances

source
class MeasureTheory.Measure.IsHaarMeasure {G : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] (μ : Measure G) extends MeasureTheory.IsFiniteMeasureOnCompacts μ, μ.IsMulLeftInvariant, μ.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.

Textbooks generally require an additional regularity assumption to ensure nice behavior on arbitrary locally compact groups. Use `[IsHaarMeasure μ] [Regular μ]` or `[IsHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our sense is automatically regular and inner regular on second countable locally compact groups, as checked just below this definition.

- lt_top_of_isCompact ⦃K : Set G⦄ : IsCompact K → μ K < ⊤
- map_mul_left_eq_self (g : G) : map (fun (x : G) => g * x) μ = μ
- open_pos (U : Set G) : IsOpen U → U.Nonempty → μ U ≠ 0

Instances

source
@[simp]
theorem MeasureTheory.Measure.haar_singleton {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : Measure G) [μ.IsHaarMeasure] [ContinuousMul G] [BorelSpace G] (g : G) :
μ {g} = μ {1}
source
@[simp]
theorem MeasureTheory.Measure.addHaar_singleton {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [ContinuousAdd G] [BorelSpace G] (g : G) :
μ {g} = μ {0}
source
theorem MeasureTheory.Measure.IsHaarMeasure.smul {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : Measure G) [μ.IsHaarMeasure] {c : ENNReal} (cpos : c ≠ 0) (ctop : c ≠ ⊤) :
(c • μ).IsHaarMeasure
source
theorem MeasureTheory.Measure.IsAddHaarMeasure.smul {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] {c : ENNReal} (cpos : c ≠ 0) (ctop : c ≠ ⊤) :
(c • μ).IsAddHaarMeasure
source
theorem MeasureTheory.Measure.IsHaarMeasure.nnreal_smul {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : Measure G) [μ.IsHaarMeasure] {c : NNReal} (hc : c ≠ 0) :
(c • μ).IsHaarMeasure
source
theorem MeasureTheory.Measure.IsAddHaarMeasure.nnreal_smul {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] {c : NNReal} (hc : c ≠ 0) :
(c • μ).IsAddHaarMeasure
source
theorem MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] (μ : Measure G) [μ.IsMulLeftInvariant] (K : Set G) (hK : IsCompact K) (h'K : (interior K).Nonempty) (h : μ K ≠ 0) (h' : μ K ≠ ⊤) :
μ.IsHaarMeasure

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

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

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

source
theorem MeasureTheory.Measure.isHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (h_surj : Function.Surjective ⇑f) (h_prop : Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H)) :
(map (⇑f) μ).IsHaarMeasure

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

source
theorem MeasureTheory.Measure.isAddHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalAddGroup H] (f : G →+ H) (hf : Continuous ⇑f) (h_surj : Function.Surjective ⇑f) (h_prop : Filter.Tendsto (⇑f) (Filter.cocompact G) (Filter.cocompact H)) :
(map (⇑f) μ).IsAddHaarMeasure

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`, `ContinuousAddEquiv.isAddHaarMeasure_map` and `ContinuousLinearEquiv.isAddHaarMeasure_map`.

source
theorem MeasureTheory.Measure.IsHaarMeasure.comap {G : Type u_1} {H : Type u_2} [MeasurableSpace G] [MeasurableSpace H] [Group G] [TopologicalSpace G] [BorelSpace G] [MeasurableMul G] [Group H] [TopologicalSpace H] [BorelSpace H] {mH : MeasurableMul H} (μ : Measure H) [μ.IsHaarMeasure] {f : G →* H} (hf : Topology.IsOpenEmbedding ⇑f) :
(comap (⇑f) μ).IsHaarMeasure
source
theorem MeasureTheory.Measure.isHaarMeasure_map_of_isFiniteMeasure {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [ContinuousMul H] [IsFiniteMeasure μ] (f : G →* H) (hf : Continuous ⇑f) (h_surj : Function.Surjective ⇑f) :
(map (⇑f) μ).IsHaarMeasure

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

source
theorem MeasureTheory.Measure.isAddHaarMeasure_map_of_isFiniteMeasure {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [ContinuousAdd H] [IsFiniteMeasure μ] (f : G →+ H) (hf : Continuous ⇑f) (h_surj : Function.Surjective ⇑f) :
(map (⇑f) μ).IsAddHaarMeasure

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

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

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

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

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

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

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

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

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

source
theorem MulEquiv.isHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [ContinuousMul G] {H : Type u_3} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (e : G ≃* H) (he : Continuous ⇑e) (hesymm : Continuous ⇑e.symm) :
(MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure

A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`.

source
theorem AddEquiv.isAddHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [ContinuousAdd G] {H : Type u_3} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalAddGroup H] (e : G ≃+ H) (he : Continuous ⇑e) (hesymm : Continuous ⇑e.symm) :
(MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure

A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`.

source
instance ContinuousMulEquiv.isHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [IsTopologicalGroup G] {H : Type u_3} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) :
(MeasureTheory.Measure.map (⇑e) μ).IsHaarMeasure

A convenience wrapper for MeasureTheory.Measure.isHaarMeasure_map.

source
instance ContinuousAddEquiv.isAddHaarMeasure_map {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [IsTopologicalAddGroup G] {H : Type u_3} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalAddGroup H] (e : G ≃ₜ+ H) :
(MeasureTheory.Measure.map (⇑e) μ).IsAddHaarMeasure

A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map.

source
instance ContinuousLinearEquiv.isAddHaarMeasure_map {E : Type u_3} {F : Type u_4} {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module S F] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (L : E ≃SL[σ] F) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] :
(MeasureTheory.Measure.map (⇑L) μ).IsAddHaarMeasure

A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`.

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

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

See Note [lower instance priority]

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

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

See Note [lower instance priority]

source
instance MeasureTheory.Measure.prod.instIsHaarMeasure {G : Type u_3} [Group G] [TopologicalSpace G] {x✝ : MeasurableSpace G} {H : Type u_4} [Group H] [TopologicalSpace H] {x✝¹ : MeasurableSpace H} (μ : Measure G) (ν : Measure H) [μ.IsHaarMeasure] [ν.IsHaarMeasure] [SFinite μ] [SFinite ν] [MeasurableMul G] [MeasurableMul H] :
(μ.prod ν).IsHaarMeasure
source
instance MeasureTheory.Measure.prod.instIsAddHaarMeasure {G : Type u_3} [AddGroup G] [TopologicalSpace G] {x✝ : MeasurableSpace G} {H : Type u_4} [AddGroup H] [TopologicalSpace H] {x✝¹ : MeasurableSpace H} (μ : Measure G) (ν : Measure H) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure] [SFinite μ] [SFinite ν] [MeasurableAdd G] [MeasurableAdd H] :
(μ.prod ν).IsAddHaarMeasure
source
@[instance 100]
instance MeasureTheory.Measure.IsHaarMeasure.noAtoms {G : Type u_1} [MeasurableSpace G] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 1 {1}ᶜ).NeBot] (μ : Measure G) [μ.IsHaarMeasure] :
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.

source
@[instance 100]
instance MeasureTheory.Measure.IsAddHaarMeasure.noAtoms {G : Type u_1} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] [T1Space G] [WeaklyLocallyCompactSpace G] [(nhdsWithin 0 {0}ᶜ).NeBot] (μ : Measure G) [μ.IsAddHaarMeasure] :
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.

source
instance MeasureTheory.Measure.IsAddHaarMeasure.domSMul {G : Type u_3} {A : Type u_4} [Group G] [AddCommGroup A] [DistribMulAction G A] [MeasurableSpace A] [TopologicalSpace A] [BorelSpace A] [IsTopologicalAddGroup A] [ContinuousConstSMul G A] {μ : Measure A} [μ.IsAddHaarMeasure] (g : G ᵈᵐᵃ) :
(g • μ).IsAddHaarMeasure