Documentation

Mathlib.MeasureTheory.Group.Defs

Definitions about invariant measures #

In this file we define typeclasses for measures invariant under (scalar) multiplication.

For basic facts about the first two typeclasses, see Mathlib/MeasureTheory/Group/Action. For facts about left/right-invariant measures, see Mathlib/MeasureTheory/Group/Measure.

Implementation Notes #

The smul/vadd typeclasses and the left/right multiplication typeclasses were defined by different people with different tastes, so the former explicitly use measures of the preimages, while the latter use MeasureTheory.Measure.map.

If the left/right multiplication is measurable (which is the case in most if not all interesting examples), these definitions are equivalent.

The definitions that use MeasureTheory.Measure.map imply that the left (resp., right) multiplication is AEMeasurable.

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

      A measure μ on a measurable additive group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

      Instances
        theorem MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self {G : Type u_1} :
        ∀ {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddLeftInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => g + x) μ = μ

        A measure μ on a measurable group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

        Instances
          theorem MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self {G : Type u_1} :
          ∀ {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulLeftInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => g * x) μ = μ

          A measure μ on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

          Instances
            theorem MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self {G : Type u_1} :
            ∀ {inst : MeasurableSpace G} {inst_1 : Add G} {μ : MeasureTheory.Measure G} [self : μ.IsAddRightInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => x + g) μ = μ

            A measure μ on a measurable group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

            Instances
              theorem MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self {G : Type u_1} :
              ∀ {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulRightInvariant] (g : G), MeasureTheory.Measure.map (fun (x : G) => x * g) μ = μ