Documentation

Mathlib.MeasureTheory.Group.Action

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.

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

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.

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

    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.

    • measure_preimage_smul : ∀ (c : M) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ ((fun (x : α) => c • x) ⁻¹' s) = ↑↑μ s
    Instances
      source
      instance MeasureTheory.VAddInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [VAdd M α] :
      MeasureTheory.VAddInvariantMeasure M α 0
      Equations
      source
      instance MeasureTheory.SMulInvariantMeasure.zero {M : Type v} {α : Type w} [MeasurableSpace α] [SMul M α] :
      MeasureTheory.SMulInvariantMeasure M α 0
      Equations
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      @[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
      source
      @[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
      source
      @[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) μ = μ
      source
      @[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) μ = μ
      source
      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 μ)
      source
      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 μ)
      source
      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
      • One or more equations did not get rendered due to their size.
      source
      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
      • One or more equations did not get rendered due to their size.
      source
      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.

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

      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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)
      source
      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)
      source
      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
      source
      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
      source
      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.

      source
      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 : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U) → Prop) :
      ∀ (x : ∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U), (∀ (t : Finset G) (ht : K ⊆ ⋃ g ∈ t, g +ᵥ U), motive (_ : ∃ (I : Finset G), K ⊆ ⋃ g ∈ I, g +ᵥ U)) → motive x
      Equations
      • (_ : motive x) = (_ : motive x)
      Instances For
        source
        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.

        source
        abbrev MeasureTheory.isLocallyFiniteMeasure_of_vaddInvariant.match_1 (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {U : Set α} (x : α) (motive : (∃ (c : G), c +ᵥ x ∈ U) → Prop) :
        ∀ (x_1 : ∃ (c : G), c +ᵥ x ∈ U), (∀ (g : G) (hg : g +ᵥ x ∈ U), motive (_ : ∃ (c : G), c +ᵥ x ∈ U)) → motive x_1
        Equations
        • (_ : motive x) = (_ : motive x)
        Instances For
          source
          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 μ
          source
          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 μ
          source
          abbrev MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero.match_1 {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] (motive : (∃ (K : Set α), IsCompact K ∧ ↑↑μ K ≠ 0) → Prop) :
          ∀ (x : ∃ (K : Set α), IsCompact K ∧ ↑↑μ K ≠ 0), (∀ (_K : Set α) (hK : IsCompact _K) (hμK : ↑↑μ _K ≠ 0), motive (_ : ∃ (K : Set α), IsCompact K ∧ ↑↑μ K ≠ 0)) → motive x
          Equations
          • (_ : motive x) = (_ : motive x)
          Instances For
            source
            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
            source
            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
            source
            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
            source
            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
            source
            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 = ∅
            source
            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 = ∅
            source
            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
            source
            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
            source
            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
            source
            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