Measures invariant under group actions

A measure μ : Measure α is said to be invariant under an action of a group G if scalar multiplication by c : G is a measure-preserving map for all c. In this file we define a typeclass for measures invariant under action of an (additive or multiplicative) group and prove some basic properties of such measures.

instance MeasureTheory.SMulInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [SMul M α] : SMulInvariantMeasure M α 0

instance MeasureTheory.VAddInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [VAdd M α] : VAddInvariantMeasure M α 0

instance MeasureTheory.SMulInvariantMeasure.add {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ ν : Measure α} [SMulInvariantMeasure M α μ] [SMulInvariantMeasure M α ν] : SMulInvariantMeasure M α (μ + ν)

instance MeasureTheory.VAddInvariantMeasure.add {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ ν : Measure α} [VAddInvariantMeasure M α μ] [VAddInvariantMeasure M α ν] : VAddInvariantMeasure M α (μ + ν)

instance MeasureTheory.SMulInvariantMeasure.smul {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ : Measure α} [SMulInvariantMeasure M α μ] (c : ENNReal) : SMulInvariantMeasure M α (c • μ)

instance MeasureTheory.VAddInvariantMeasure.vadd {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ : Measure α} [VAddInvariantMeasure M α μ] (c : ENNReal) : VAddInvariantMeasure M α (c • μ)

instance MeasureTheory.SMulInvariantMeasure.smul_nnreal {M : Type v} {α : Type w} [SMul M α] {m : MeasurableSpace α} {μ : Measure α} [SMulInvariantMeasure M α μ] (c : NNReal) : SMulInvariantMeasure M α (c • μ)

instance MeasureTheory.VAddInvariantMeasure.vadd_nnreal {M : Type v} {α : Type w} [VAdd M α] {m : MeasurableSpace α} {μ : Measure α} [VAddInvariantMeasure M α μ] (c : NNReal) : VAddInvariantMeasure M α (c • μ)

theorem MeasureTheory.measure_preimage_smul_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] (μ : Measure α) [SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c • x) ⁻¹' s) ≤ μ s

See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.

theorem MeasureTheory.measure_preimage_vadd_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : Measure α) [VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) ≤ μ s

See also measure_preimage_smul_of_nullMeasurableSet and measure_preimage_smul.

theorem MeasureTheory.tendsto_smul_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] (μ : Measure α) [SMulInvariantMeasure G α μ] (c : G) : Filter.Tendsto (fun (x : α) => c • x) (ae μ) (ae μ)

See also smul_ae.

theorem MeasureTheory.tendsto_vadd_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : Measure α) [VAddInvariantMeasure G α μ] (c : G) : Filter.Tendsto (fun (x : α) => c +ᵥ x) (ae μ) (ae μ)

See also vadd_ae.

theorem MeasureTheory.measure_preimage_smul_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ ((fun (x : α) => c • x) ⁻¹' s) = 0

theorem MeasureTheory.measure_preimage_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : Measure α} [VAddInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = 0

theorem MeasureTheory.measure_preimage_smul_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : Measure α} [SMulInvariantMeasure G α μ] {s : Set α} (hs : NullMeasurableSet s μ) (c : G) : μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

theorem MeasureTheory.measure_preimage_vadd_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : Measure α} [VAddInvariantMeasure G α μ] {s : Set α} (hs : NullMeasurableSet s μ) (c : G) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_preimage_smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure α) [SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c • x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_preimage_vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : Measure α) [VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s

@[simp]

theorem MeasureTheory.measure_smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure α) [SMulInvariantMeasure G α μ] (c : G) (s : Set α) : μ (c • s) = μ s

@[simp]

theorem MeasureTheory.measure_vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : Measure α) [VAddInvariantMeasure G α μ] (c : G) (s : Set α) : μ (c +ᵥ s) = μ s

theorem MeasureTheory.measure_smul_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] {s : Set α} (c : G) : μ (c • s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_vadd_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] {s : Set α} (c : G) : μ (c +ᵥ s) = 0 ↔ μ s = 0

theorem MeasureTheory.measure_smul_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ (c • s) = 0

theorem MeasureTheory.measure_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) : μ (c +ᵥ s) = 0

@[simp]

theorem MeasureTheory.smul_mem_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (c : G) {s : Set α} : c • s ∈ ae μ ↔ s ∈ ae μ

@[simp]

theorem MeasureTheory.vadd_mem_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (c : G) {s : Set α} : c +ᵥ s ∈ ae μ ↔ s ∈ ae μ

@[simp]

theorem MeasureTheory.smul_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (c : G) : c • ae μ = ae μ

@[simp]

theorem MeasureTheory.vadd_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (c : G) : c +ᵥ ae μ = ae μ

@[simp]

theorem MeasureTheory.eventuallyConst_smul_set_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (c : G) {s : Set α} : Filter.EventuallyConst (c • s) (ae μ) ↔ Filter.EventuallyConst s (ae μ)

@[simp]

theorem MeasureTheory.eventuallyConst_vadd_set_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (c : G) {s : Set α} : Filter.EventuallyConst (c +ᵥ s) (ae μ) ↔ Filter.EventuallyConst s (ae μ)

@[simp]

theorem MeasureTheory.smul_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (c : G) {s t : Set α} : c • s ≤ᶠ[ae μ] c • t ↔ s ≤ᶠ[ae μ] t

@[simp]

theorem MeasureTheory.vadd_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (c : G) {s t : Set α} : c +ᵥ s ≤ᶠ[ae μ] c +ᵥ t ↔ s ≤ᶠ[ae μ] t

@[simp]

theorem MeasureTheory.smul_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] (c : G) {s t : Set α} : c • s =ᶠ[ae μ] c • t ↔ s =ᶠ[ae μ] t

@[simp]

theorem MeasureTheory.vadd_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] (c : G) {s t : Set α} : c +ᵥ s =ᶠ[ae μ] c +ᵥ t ↔ s =ᶠ[ae μ] t

@[simp]

theorem MeasureTheory.measurePreserving_smul {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [SMul M α] [MeasurableSMul M α] (c : M) (μ : Measure α) [SMulInvariantMeasure M α μ] : MeasurePreserving (fun (x : α) => c • x) μ μ

@[simp]

theorem MeasureTheory.measurePreserving_vadd {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [VAdd M α] [MeasurableVAdd M α] (c : M) (μ : Measure α) [VAddInvariantMeasure M α μ] : MeasurePreserving (fun (x : α) => c +ᵥ x) μ μ

@[simp]

theorem MeasureTheory.map_smul {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [SMul M α] [MeasurableSMul M α] (c : M) (μ : Measure α) [SMulInvariantMeasure M α μ] : Measure.map (fun (x : α) => c • x) μ = μ

@[simp]

theorem MeasureTheory.map_vadd {M : Type v} {α : Type w} {m : MeasurableSpace α} [MeasurableSpace M] [VAdd M α] [MeasurableVAdd M α] (c : M) (μ : Measure α) [VAddInvariantMeasure M α μ] : Measure.map (fun (x : α) => c +ᵥ x) μ = μ

theorem MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct {α : Type w} {f : α → α} {x✝ : MeasurableSpace α} {μ : Measure α} (hf : MeasurePreserving f μ μ) : SMulInvariantMeasure (IterateMulAct f) α μ

theorem MeasureTheory.MeasurePreserving.vaddInvariantMeasure_iterateAddAct {α : Type w} {f : α → α} {x✝ : MeasurableSpace α} {μ : Measure α} (hf : MeasurePreserving f μ μ) : VAddInvariantMeasure (IterateAddAct f) α μ

theorem MeasureTheory.smulInvariantMeasure_iterateMulAct {α : Type w} {f : α → α} {x✝ : MeasurableSpace α} {μ : Measure α} (hf : Measurable f) : SMulInvariantMeasure (IterateMulAct f) α μ ↔ MeasurePreserving f μ μ

theorem MeasureTheory.vaddInvariantMeasure_iterateAddAct {α : Type w} {f : α → α} {x✝ : MeasurableSpace α} {μ : Measure α} (hf : Measurable f) : VAddInvariantMeasure (IterateAddAct f) α μ ↔ MeasurePreserving f μ μ

theorem MeasureTheory.smulInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [SMul M α] [SMul M β] [MeasurableSMul M β] (μ : Measure α) [SMulInvariantMeasure M α μ] (f : α → β) (hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a) (hf : Measurable f) : SMulInvariantMeasure M β (Measure.map f μ)

theorem MeasureTheory.vaddInvariantMeasure_map {M : Type uM} {α : Type uα} {β : Type uβ} [MeasurableSpace M] [MeasurableSpace α] [MeasurableSpace β] [VAdd M α] [VAdd M β] [MeasurableVAdd M β] (μ : Measure α) [VAddInvariantMeasure M α μ] (f : α → β) (hvadd : ∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) (hf : Measurable f) : VAddInvariantMeasure M β (Measure.map f μ)

instance MeasureTheory.smulInvariantMeasure_map_smul {M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [SMul M α] [SMul N α] [SMulCommClass N M α] [MeasurableSMul M α] [MeasurableSMul N α] (μ : Measure α) [SMulInvariantMeasure M α μ] (n : N) : SMulInvariantMeasure M α (Measure.map (fun (x : α) => n • x) μ)

instance MeasureTheory.vaddInvariantMeasure_map_vadd {M : Type uM} {N : Type uN} {α : Type uα} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [VAdd M α] [VAdd N α] [VAddCommClass N M α] [MeasurableVAdd M α] [MeasurableVAdd N α] (μ : Measure α) [VAddInvariantMeasure M α μ] (n : N) : VAddInvariantMeasure M α (Measure.map (fun (x : α) => n +ᵥ x) μ)

theorem MeasureTheory.smulInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : Measure α) [MeasurableSpace G] [MeasurableSMul G α] : [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun (x : α) => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), Measure.map (fun (x : α) => c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) => c • x) μ μ].TFAE

Equivalent definitions of a measure invariant under a multiplicative action of a group.

• 0: SMulInvariantMeasure G α μ;

• 1: for every c : G and a measurable set s, the measure of the preimage of s under scalar multiplication by c is equal to the measure of s;

• 2: for every c : G and a measurable set s, the measure of the image c • s of s under scalar multiplication by c is equal to the measure of s;

• 3, 4: properties 2, 3 for any set, including non-measurable ones;

• 5: for any c : G, scalar multiplication by c maps μ to μ;

• 6: for any c : G, scalar multiplication by c is a measure-preserving map.

theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : Measure α) [MeasurableSpace G] [MeasurableVAdd G α] : [VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s, ∀ (c : G) (s : Set α), μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s, ∀ (c : G), Measure.map (fun (x : α) => c +ᵥ x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) => c +ᵥ x) μ μ].TFAE

Equivalent definitions of a measure invariant under an additive action of a group.

• 0: VAddInvariantMeasure G α μ;

• 1: for every c : G and a measurable set s, the measure of the preimage of s under vector addition (c +ᵥ ·) is equal to the measure of s;

• 2: for every c : G and a measurable set s, the measure of the image c +ᵥ s of s under vector addition (c +ᵥ ·) is equal to the measure of s;

• 3, 4: properties 2, 3 for any set, including non-measurable ones;

• 5: for any c : G, vector addition of c maps μ to μ;

• 6: for any c : G, vector addition of c is a measure-preserving map.

theorem MeasureTheory.NullMeasurableSet.smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [MeasurableSpace G] [MeasurableSMul G α] {s : Set α} (hs : NullMeasurableSet s μ) (c : G) : NullMeasurableSet (c • s) μ

theorem MeasureTheory.NullMeasurableSet.vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [MeasurableSpace G] [MeasurableVAdd G α] {s : Set α} (hs : NullMeasurableSet s μ) (c : G) : NullMeasurableSet (c +ᵥ s) μ

theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {K U : Set α} (hK : IsCompact K) (hμK : μ K ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

If measure μ is invariant under a group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero.

theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {K U : Set α} (hK : IsCompact K) (hμK : μ K ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

If measure μ is invariant under an additive group action and is nonzero on a compact set K, then it is positive on any nonempty open set. In case of a regular measure, one can assume μ ≠ 0 instead of μ K ≠ 0, see MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.

theorem MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ⊤) : IsLocallyFiniteMeasure μ

theorem MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} (hU : IsOpen U) (hne : U.Nonempty) (hμU : μ U ≠ ⊤) : IsLocallyFiniteMeasure μ

theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) (hne : U.Nonempty) : 0 < μ U

theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty

theorem MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty

theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : Measure α} [SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : μ U = 0 ↔ U = ∅

theorem MeasureTheory.measure_eq_zero_iff_eq_empty_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : Measure α} [VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ ≠ 0) (hU : IsOpen U) : μ U = 0 ↔ U = ∅