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

In this file we define the following measurable equivalences:

• MeasurableEquiv.smul: if a group G acts on α by measurable maps, then each element c : G defines a measurable automorphism of α;
• MeasurableEquiv.vadd: additive version of MeasurableEquiv.smul;
• MeasurableEquiv.smul₀: if a group with zero G acts on α by measurable maps, then each nonzero element c : G defines a measurable automorphism of α;
• MeasurableEquiv.mulLeft: if G is a group with measurable multiplication, then left multiplication by g : G is a measurable automorphism of G;
• MeasurableEquiv.addLeft: additive version of MeasurableEquiv.mulLeft;
• MeasurableEquiv.mulRight: if G is a group with measurable multiplication, then right multiplication by g : G is a measurable automorphism of G;
• MeasurableEquiv.addRight: additive version of MeasurableEquiv.mulRight;
• MeasurableEquiv.mulLeft₀, MeasurableEquiv.mulRight₀: versions of MeasurableEquiv.mulLeft and MeasurableEquiv.mulRight for groups with zero;
• MeasurableEquiv.inv: Inv.inv as a measurable automorphism of a group (or a group with zero);
• MeasurableEquiv.neg: negation as a measurable automorphism of an additive group.

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} [] [] [] [] [] (c : G) :
Measurable fun (x : α) => c +ᵥ x
def MeasurableEquiv.vadd {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
α ≃ᵐ α

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

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem MeasurableEquiv.vadd.proof_2 {G : Type u_2} {α : Type u_1} [] [] [] [] [] (c : G) :
Measurable fun (x : α) => -c +ᵥ x
@[simp]
theorem MeasurableEquiv.vadd_apply {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
= fun (x : α) => c +ᵥ x
@[simp]
theorem MeasurableEquiv.vadd_toEquiv {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
.toEquiv =
@[simp]
theorem MeasurableEquiv.smul_apply {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
= fun (x : α) => c x
@[simp]
theorem MeasurableEquiv.smul_toEquiv {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
.toEquiv =
def MeasurableEquiv.smul {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
α ≃ᵐ α

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

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem measurableEmbedding_const_vadd {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
MeasurableEmbedding fun (x : α) => c +ᵥ x
theorem measurableEmbedding_const_smul {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
MeasurableEmbedding fun (x : α) => c x
@[simp]
theorem MeasurableEquiv.symm_vadd {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
.symm =
@[simp]
theorem MeasurableEquiv.symm_smul {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
.symm =
def MeasurableEquiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction 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} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
() = fun (x : α) => c x
@[simp]
theorem MeasurableEquiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
().symm =
theorem measurableEmbedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
MeasurableEmbedding fun (x : α) => c x
theorem MeasurableEquiv.addLeft.proof_1 {G : Type u_1} [] [] [] :
def MeasurableEquiv.addLeft {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ G

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} [] [] [] (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} [] [] [] (g : G) :
= fun (x : G) => g + x
@[simp]
theorem MeasurableEquiv.coe_mulLeft {G : Type u_1} [] [] [] (g : G) :
= fun (x : G) => g * x
@[simp]
theorem MeasurableEquiv.symm_addLeft {G : Type u_1} [] [] [] (g : G) :
.symm =
@[simp]
theorem MeasurableEquiv.symm_mulLeft {G : Type u_1} [] [] [] (g : G) :
@[simp]
theorem MeasurableEquiv.toEquiv_addLeft {G : Type u_1} [] [] [] (g : G) :
.toEquiv =
@[simp]
theorem MeasurableEquiv.toEquiv_mulLeft {G : Type u_1} [] [] [] (g : G) :
.toEquiv =
theorem measurableEmbedding_addLeft {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun (x : G) => g + x
theorem measurableEmbedding_mulLeft {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun (x : G) => g * x
def MeasurableEquiv.addRight {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ 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
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem MeasurableEquiv.addRight.proof_1 {G : Type u_1} [] [] [] (g : G) :
Measurable fun (x : G) => x + g
theorem MeasurableEquiv.addRight.proof_2 {G : Type u_1} [] [] [] (g : G) :
Measurable fun (x : G) => x + -g
def MeasurableEquiv.mulRight {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ G

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

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem measurableEmbedding_addRight {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun (x : G) => x + g
theorem measurableEmbedding_mulRight {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun (x : G) => x * g
@[simp]
theorem MeasurableEquiv.coe_addRight {G : Type u_1} [] [] [] (g : G) :
= fun (x : G) => x + g
@[simp]
theorem MeasurableEquiv.coe_mulRight {G : Type u_1} [] [] [] (g : G) :
= fun (x : G) => x * g
@[simp]
theorem MeasurableEquiv.symm_addRight {G : Type u_1} [] [] [] (g : G) :
.symm =
@[simp]
theorem MeasurableEquiv.symm_mulRight {G : Type u_1} [] [] [] (g : G) :
@[simp]
theorem MeasurableEquiv.toEquiv_addRight {G : Type u_1} [] [] [] (g : G) :
.toEquiv =
@[simp]
theorem MeasurableEquiv.toEquiv_mulRight {G : Type u_1} [] [] [] (g : G) :
.toEquiv =
def MeasurableEquiv.mulLeft₀ {G₀ : Type u_2} [] [] [] (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} [] [] [] {g : G₀} (hg : g 0) :
MeasurableEmbedding fun (x : G₀) => g * x
@[simp]
theorem MeasurableEquiv.coe_mulLeft₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
() = fun (x : G₀) => g * x
@[simp]
theorem MeasurableEquiv.symm_mulLeft₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
().symm =
@[simp]
theorem MeasurableEquiv.toEquiv_mulLeft₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
().toEquiv =
def MeasurableEquiv.mulRight₀ {G₀ : Type u_2} [] [] [] (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
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem measurableEmbedding_mulRight₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
MeasurableEmbedding fun (x : G₀) => x * g
@[simp]
theorem MeasurableEquiv.coe_mulRight₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
() = fun (x : G₀) => x * g
@[simp]
theorem MeasurableEquiv.symm_mulRight₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
().symm =
@[simp]
theorem MeasurableEquiv.toEquiv_mulRight₀ {G₀ : Type u_2} [] [] [] {g : G₀} (hg : g 0) :
().toEquiv =
def MeasurableEquiv.neg (G : Type u_4) [] [] [] :
G ≃ᵐ G

Negation as a measurable automorphism of an additive group.

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem MeasurableEquiv.neg.proof_1 (G : Type u_1) [] [] [] :
Measurable Neg.neg
@[simp]
theorem MeasurableEquiv.neg_toEquiv (G : Type u_4) [] [] [] :
.toEquiv =
@[simp]
theorem MeasurableEquiv.inv_toEquiv (G : Type u_4) [] [] [] :
.toEquiv =
@[simp]
theorem MeasurableEquiv.inv_apply (G : Type u_4) [] [] [] :
= Inv.inv
@[simp]
theorem MeasurableEquiv.neg_apply (G : Type u_4) [] [] [] :
= Neg.neg
def MeasurableEquiv.inv (G : Type u_4) [] [] [] :
G ≃ᵐ G

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

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
@[simp]
theorem MeasurableEquiv.symm_neg {G : Type u_4} [] [] [] :
.symm =
@[simp]
theorem MeasurableEquiv.symm_inv {G : Type u_4} [] [] [] :
.symm =
theorem MeasurableEquiv.subRight.proof_2 {G : Type u_1} [] [] [] (g : G) :
Measurable fun (x : G) => x + g
theorem MeasurableEquiv.subRight.proof_1 {G : Type u_1} [] [] [] (g : G) :
Measurable fun (h : G) => h - g
def MeasurableEquiv.subRight {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ G

equiv.subRight as a MeasurableEquiv

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
def MeasurableEquiv.divRight {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ G

equiv.divRight as a MeasurableEquiv.

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
theorem MeasurableEquiv.subLeft.proof_2 {G : Type u_1} [] [] [] [] (g : G) :
Measurable fun (x : G) => -x + g
theorem MeasurableEquiv.subLeft.proof_1 {G : Type u_1} [] [] [] [] (g : G) :
Measurable fun (x : G) => g - id x
def MeasurableEquiv.subLeft {G : Type u_1} [] [] [] [] (g : G) :
G ≃ᵐ G

equiv.subLeft as a MeasurableEquiv

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For
def MeasurableEquiv.divLeft {G : Type u_1} [] [] [] [] (g : G) :
G ≃ᵐ G

equiv.divLeft as a MeasurableEquiv

Equations
• = { toEquiv := , measurable_toFun := , measurable_invFun := }
Instances For