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.

class MeasureTheory.VAddInvariantMeasure (M : Type u_1) (α : Type u_2) [VAdd M α] :

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
    theorem MeasureTheory.VAddInvariantMeasure.measure_preimage_vadd {M : Type u_1} {α : Type u_2} [VAdd M α] :
    ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.VAddInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet sμ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
    class MeasureTheory.SMulInvariantMeasure (M : Type u_1) (α : Type u_2) [SMul M α] :

    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.

    Instances
      theorem MeasureTheory.SMulInvariantMeasure.measure_preimage_smul {M : Type u_1} {α : Type u_2} [SMul M α] :
      ∀ {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.SMulInvariantMeasure M α μ] (c : M) ⦃s : Set α⦄, MeasurableSet sμ ((fun (x : α) => c x) ⁻¹' s) = μ s
      theorem MeasureTheory.measure_preimage_vadd_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : MeasureTheory.Measure α) [MeasureTheory.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.measure_preimage_smul_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] (μ : MeasureTheory.Measure α) [MeasureTheory.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.tendsto_vadd_ae {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) :
      Filter.Tendsto (fun (x : α) => c +ᵥ x) (MeasureTheory.ae μ) (MeasureTheory.ae μ)

      See also vadd_ae.

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

      See also smul_ae.

      theorem MeasureTheory.measure_preimage_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) :
      μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = 0
      theorem MeasureTheory.measure_preimage_smul_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) :
      μ ((fun (x : α) => c x) ⁻¹' s) = 0
      theorem MeasureTheory.measure_preimage_vadd_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [VAdd G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) :
      μ ((fun (x : α) => c +ᵥ x) ⁻¹' s) = μ s
      theorem MeasureTheory.measure_preimage_smul_of_nullMeasurableSet {G : Type u} {α : Type w} {m : MeasurableSpace α} [SMul G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) (c : G) :
      μ ((fun (x : α) => c x) ⁻¹' s) = μ s
      @[simp]
      theorem MeasureTheory.measure_preimage_vadd {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : 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 α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : 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 α] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α) :
      μ (c +ᵥ s) = μ s
      @[simp]
      theorem MeasureTheory.measure_smul {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α) :
      μ (c s) = μ s
      theorem MeasureTheory.measure_vadd_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] {s : Set α} (c : G) :
      μ (c +ᵥ s) = 0 μ s = 0
      theorem MeasureTheory.measure_smul_eq_zero_iff {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (c : G) :
      μ (c s) = 0 μ s = 0
      theorem MeasureTheory.measure_vadd_null {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction 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 α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] {s : Set α} (h : μ s = 0) (c : G) :
      μ (c s) = 0
      @[simp]
      @[simp]
      @[simp]
      theorem MeasureTheory.vadd_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} :
      c +ᵥ s ≤ᵐ[μ] c +ᵥ t s ≤ᵐ[μ] t
      @[simp]
      theorem MeasureTheory.smul_set_ae_le {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} :
      c s ≤ᵐ[μ] c t s ≤ᵐ[μ] t
      @[simp]
      theorem MeasureTheory.vadd_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} :
      c +ᵥ s =ᵐ[μ] c +ᵥ t s =ᵐ[μ] t
      @[simp]
      theorem MeasureTheory.smul_set_ae_eq {G : Type u} {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) {s : Set α} {t : Set α} :
      c s =ᵐ[μ] c t s =ᵐ[μ] t
      @[simp]
      @[simp]
      @[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) :
      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) :
      Equations
      • =
      theorem MeasureTheory.vaddInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] [MeasurableSpace G] [MeasurableVAdd G α] (μ : MeasureTheory.Measure α) :
      [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) μ μ].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.smulInvariantMeasure_tfae (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] [MeasurableSpace G] [MeasurableSMul G α] (μ : MeasureTheory.Measure α) :
      [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) μ μ].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.

      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 gI, g +ᵥ U)Prop) :
      ∀ (x : ∃ (I : Finset G), K gI, g +ᵥ U), (∀ (t : Finset G) (ht : K gt, g +ᵥ U), motive )motive x
      Equations
      • =
      Instances For
        theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction 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 : 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.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction 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 : 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.

        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 )motive x_1
        Equations
        • =
        Instances For
          theorem MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : IsOpen U) (hne : U.Nonempty) :
          0 < μ U
          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 )motive x
          Equations
          • =
          Instances For
            theorem MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : IsOpen U) (hne : U.Nonempty) :
            0 < μ U
            theorem MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : IsOpen U) :
            0 < μ U U.Nonempty
            theorem MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.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 α] {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [TopologicalSpace α] [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α} [μ.Regular] (hμ : μ 0) (hU : IsOpen U) :
            μ U = 0 U =