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.

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] : {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop

• measure_preimage_vadd : ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ ((fun x => c +ᵥ x) ⁻¹' s) = ↑↑μ s

A measure μ : Measure α is invariant under an additive action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c +ᵥ x is equal to the measure of s.

class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] : {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop

• measure_preimage_smul : ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s

A measure μ : Measure α is invariant under a multiplicative action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c • x is equal to the measure of s.

theorem MeasureTheory.VAddInvariantMeasure.zero.proof_1 {M : Type u_1} {α : Type u_2} [MeasurableSpace α] [VAdd M α] : MeasureTheory.VAddInvariantMeasure M α 0

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

Equations

• @MeasureTheory.VAddInvariantMeasure.zero = @MeasureTheory.VAddInvariantMeasure.zero.proof_1

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

Equations

• @MeasureTheory.SMulInvariantMeasure.zero = @MeasureTheory.SMulInvariantMeasure.zero.proof_1

theorem MeasureTheory.VAddInvariantMeasure.add.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] [MeasureTheory.VAddInvariantMeasure M α ν] : MeasureTheory.VAddInvariantMeasure M α (μ + ν)

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

Equations

• @MeasureTheory.VAddInvariantMeasure.add = @MeasureTheory.VAddInvariantMeasure.add.proof_1

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

Equations

• @MeasureTheory.SMulInvariantMeasure.add = @MeasureTheory.SMulInvariantMeasure.add.proof_1

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

Equations

• @MeasureTheory.VAddInvariantMeasure.vadd = @MeasureTheory.VAddInvariantMeasure.vadd.proof_1

theorem MeasureTheory.VAddInvariantMeasure.vadd.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] (c : ENNReal) : MeasureTheory.VAddInvariantMeasure M α (c • μ)

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

Equations

• @MeasureTheory.SMulInvariantMeasure.smul = @MeasureTheory.SMulInvariantMeasure.smul.proof_1

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

Equations

• @MeasureTheory.VAddInvariantMeasure.vadd_nnreal = @MeasureTheory.VAddInvariantMeasure.vadd_nnreal.proof_1

theorem MeasureTheory.VAddInvariantMeasure.vadd_nnreal.proof_1 {M : Type u_1} {α : Type u_2} [VAdd M α] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure M α μ] (c : NNReal) : MeasureTheory.VAddInvariantMeasure M α (↑c • μ)

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

Equations

• @MeasureTheory.SMulInvariantMeasure.smul_nnreal = @MeasureTheory.SMulInvariantMeasure.smul_nnreal.proof_1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem MeasureTheory.vaddInvariantMeasure_map_vadd.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [MeasurableSpace M] [MeasurableSpace N] [MeasurableSpace α] [VAdd M α] [VAdd N α] [VAddCommClass N M α] [MeasurableVAdd M α] [MeasurableVAdd N α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (n : N) : MeasureTheory.VAddInvariantMeasure M α (MeasureTheory.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 α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ] (n : N) : MeasureTheory.VAddInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n +ᵥ x) μ)

Equations

• @MeasureTheory.vaddInvariantMeasure_map_vadd = @MeasureTheory.vaddInvariantMeasure_map_vadd.proof_1

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 α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ] (n : N) : MeasureTheory.SMulInvariantMeasure M α (MeasureTheory.Measure.map (fun x => n • x) μ)

Equations

• @MeasureTheory.smulInvariantMeasure_map_smul = @MeasureTheory.smulInvariantMeasure_map_smul.proof_1

theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] (μ : MeasureTheory.Measure α) : List.TFAE [MeasureTheory.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), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving fun x => c +ᵥ x]

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.smulInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] (μ : MeasureTheory.Measure α) : List.TFAE [MeasureTheory.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), MeasureTheory.Measure.map (fun x => c • x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving fun x => c • x]

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {K : Set α} {U : Set α} (motive : (∃ I, K ⊆ ⋃ (g : G) (_ : g ∈ I), g +ᵥ U) → Prop) : (x : ∃ I, K ⊆ ⋃ (g : G) (_ : g ∈ I), g +ᵥ U) → ((t : Finset G) → (ht : K ⊆ ⋃ (g : G) (_ : g ∈ t), g +ᵥ U) → motive (_ : ∃ I, K ⊆ ⋃ (g : G) (_ : g ∈ I), g +ᵥ U)) → motive x

Equations

• MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero.match_1 G motive x h_1 = Exists.casesOn x fun w h => h_1 w h

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

abbrev MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} (x : α) (motive : (∃ c, c +ᵥ x ∈ U) → Prop) : (x : ∃ c, c +ᵥ x ∈ U) → ((g : G) → (hg : g +ᵥ x ∈ U) → motive (_ : ∃ c, c +ᵥ x ∈ U)) → motive x

Equations

• MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant.match_1 G x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

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

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

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

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

Equations

• MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.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.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [MeasureTheory.Measure.Regular μ] (hμ : μ ≠ 0) (hU : IsOpen U) (hne : Set.Nonempty U) : 0 < ↑↑μ U

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

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

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

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

theorem MeasureTheory.smul_ae_eq_self_of_mem_zpowers {G : Type u} {α : Type w} {s : Set α} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {x : G} {y : G} (hs : x • s =ᶠ[MeasureTheory.Measure.ae μ] s) (hy : y ∈ Subgroup.zpowers x) : y • s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples {G : Type u} {α : Type w} {s : Set α} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {x : G} {y : G} (hs : x +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] s) (hy : y ∈ AddSubgroup.zmultiples x) : y +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.neg_vadd_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {x : G} (hs : x +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] s) : -x +ᵥ s =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.inv_smul_ae_eq_self {G : Type u} {α : Type w} {s : Set α} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {x : G} (hs : x • s =ᶠ[MeasureTheory.Measure.ae μ] s) : x⁻¹ • s =ᶠ[MeasureTheory.Measure.ae μ] s