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 x_1 => x +ᵥ x_1) c)
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 α.

Instances For
    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 x_1 => x +ᵥ x_1) (-c))
    @[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]
    @[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) :
    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 α.

    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 x_1 => x +ᵥ x_1) c)
      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 x_1 => x x_1) c)
      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 α

      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 x_1 => x x_1) c
        @[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 x_1 => x x_1) c)

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

        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.

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

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

            Instances For

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

              Instances For
                @[simp]
                theorem MeasurableEquiv.coe_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) :
                ↑(MeasurableEquiv.addRight g) = fun x => x + g
                @[simp]
                theorem MeasurableEquiv.coe_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) :
                ↑(MeasurableEquiv.mulRight g) = fun x => 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₀.

                Instances For
                  theorem measurableEmbedding_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                  MeasurableEmbedding ((fun x x_1 => x * x_1) g)
                  @[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 x_1 => x * x_1) g
                  @[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₀.

                  Instances For
                    theorem measurableEmbedding_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g 0) :
                    MeasurableEmbedding fun x => 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 => x * g
                    @[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.

                    Instances For

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

                      Instances For

                        equiv.subRight as a MeasurableEquiv

                        Instances For

                          equiv.divRight as a MeasurableEquiv.

                          Instances For

                            equiv.subLeft as a MeasurableEquiv

                            Instances For

                              equiv.divLeft as a MeasurableEquiv

                              Instances For