Documentation

Mathlib.MeasureTheory.Group.MeasurableEquiv

(Scalar) multiplication and (vector) addition as measurable equivalences #

In this file we define the following measurable equivalences:

We also deduce that the corresponding maps are measurable embeddings.

Tags #

measurable, equivalence, group action

theorem MeasurableEquiv.vadd.proof_1 {G : Type u_2} {α : Type u_1} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) :
Measurable fun (x : α) => c +ᵥ x
theorem MeasurableEquiv.vadd.proof_2 {G : Type u_2} {α : Type u_1} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) :
Measurable fun (x : α) => -c +ᵥ x
def MeasurableEquiv.vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) :
α ≃ᵐ α

If an additive group G acts on α by measurable maps, then each element c : G defines a measurable automorphism of α.

Equations
Instances For
    @[simp]
    theorem MeasurableEquiv.smul_apply {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) :
    (MeasurableEquiv.smul c) = fun (x : α) => c x
    @[simp]
    theorem MeasurableEquiv.smul_toEquiv {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) :
    @[simp]
    theorem MeasurableEquiv.vadd_apply {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) :
    (MeasurableEquiv.vadd c) = fun (x : α) => c +ᵥ x
    @[simp]
    def MeasurableEquiv.smul {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) :
    α ≃ᵐ α

    If a group G acts on α by measurable maps, then each element c : G defines a measurable automorphism of α.

    Equations
    Instances For
      theorem measurableEmbedding_const_vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) :
      MeasurableEmbedding fun (x : α) => c +ᵥ x
      theorem measurableEmbedding_const_smul {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) :
      MeasurableEmbedding fun (x : α) => c x
      @[simp]
      def MeasurableEquiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] (c : G₀) (hc : c 0) :
      α ≃ᵐ α

      If a group with zero G₀ acts on α by measurable maps, then each nonzero element c : G₀ defines a measurable automorphism of α

      Equations
      Instances For
        @[simp]
        theorem MeasurableEquiv.coe_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c 0) :
        (MeasurableEquiv.smul₀ c hc) = fun (x : α) => c x
        @[simp]
        theorem MeasurableEquiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c 0) :
        theorem measurableEmbedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c 0) :
        MeasurableEmbedding fun (x : α) => c x

        If G is an additive group with measurable addition, then addition of g : G on the left is a measurable automorphism of G.

        Equations
        Instances For
          def MeasurableEquiv.mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
          G ≃ᵐ G

          If G is a group with measurable multiplication, then left multiplication by g : G is a measurable automorphism of G.

          Equations
          Instances For
            @[simp]
            theorem MeasurableEquiv.coe_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
            (MeasurableEquiv.addLeft g) = fun (x : G) => g + x
            @[simp]
            theorem MeasurableEquiv.coe_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
            (MeasurableEquiv.mulLeft g) = fun (x : G) => g * x
            theorem measurableEmbedding_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
            MeasurableEmbedding fun (x : G) => g + x
            theorem measurableEmbedding_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
            MeasurableEmbedding fun (x : G) => g * x
            theorem MeasurableEquiv.addRight.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
            Measurable fun (x : G) => x + -g

            If G is an additive group with measurable addition, then addition of g : G on the right is a measurable automorphism of G.

            Equations
            Instances For
              theorem MeasurableEquiv.addRight.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
              Measurable fun (x : G) => x + g

              If G is a group with measurable multiplication, then right multiplication by g : G is a measurable automorphism of G.

              Equations
              Instances For
                theorem measurableEmbedding_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
                MeasurableEmbedding fun (x : G) => x + g
                theorem measurableEmbedding_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
                MeasurableEmbedding fun (x : G) => x * g
                @[simp]
                theorem MeasurableEquiv.coe_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
                (MeasurableEquiv.addRight g) = fun (x : G) => x + g
                @[simp]
                theorem MeasurableEquiv.coe_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
                (MeasurableEquiv.mulRight g) = fun (x : G) => x * g
                def MeasurableEquiv.mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] (g : G₀) (hg : g 0) :
                G₀ ≃ᵐ G₀

                If G₀ is a group with zero with measurable multiplication, then left multiplication by a nonzero element g : G₀ is a measurable automorphism of G₀.

                Equations
                Instances For
                  theorem measurableEmbedding_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                  MeasurableEmbedding fun (x : G₀) => g * x
                  @[simp]
                  theorem MeasurableEquiv.coe_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                  (MeasurableEquiv.mulLeft₀ g hg) = fun (x : G₀) => g * x
                  @[simp]
                  @[simp]
                  theorem MeasurableEquiv.toEquiv_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                  def MeasurableEquiv.mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] (g : G₀) (hg : g 0) :
                  G₀ ≃ᵐ G₀

                  If G₀ is a group with zero with measurable multiplication, then right multiplication by a nonzero element g : G₀ is a measurable automorphism of G₀.

                  Equations
                  Instances For
                    theorem measurableEmbedding_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                    MeasurableEmbedding fun (x : G₀) => x * g
                    @[simp]
                    theorem MeasurableEquiv.coe_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                    (MeasurableEquiv.mulRight₀ g hg) = fun (x : G₀) => x * g
                    @[simp]
                    @[simp]
                    theorem MeasurableEquiv.toEquiv_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :

                    Negation as a measurable automorphism of an additive group.

                    Equations
                    Instances For

                      Inversion as a measurable automorphism of a group or group with zero.

                      Equations
                      Instances For

                        equiv.subRight as a MeasurableEquiv

                        Equations
                        Instances For
                          theorem MeasurableEquiv.subRight.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
                          Measurable fun (x : G) => x + g
                          theorem MeasurableEquiv.subRight.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
                          Measurable fun (h : G) => h - g

                          equiv.divRight as a MeasurableEquiv.

                          Equations
                          Instances For

                            equiv.subLeft as a MeasurableEquiv

                            Equations
                            Instances For
                              theorem MeasurableEquiv.subLeft.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (g : G) :
                              Measurable fun (x : G) => g - id x
                              theorem MeasurableEquiv.subLeft.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (g : G) :
                              Measurable fun (x : G) => -x + g

                              equiv.divLeft as a MeasurableEquiv

                              Equations
                              Instances For