# mathlibdocumentation

measure_theory.group.measurable_equiv

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

In this file we define the following measurable equivalences:

• measurable_equiv.smul: if a group G acts on α by measurable maps, then each element c : G defines a measurable automorphism of α;
• measurable_equiv.vadd: additive version of measurable_equiv.smul;
• measurable_equiv.smul₀: if a group with zero G acts on α by measurable maps, then each nonzero element c : G defines a measurable automorphism of α;
• measurable_equiv.mul_left: if G is a group with measurable multiplication, then left multiplication by g : G is a measurable automorphism of G;
• measurable_equiv.add_left: additive version of measurable_equiv.mul_left;
• measurable_equiv.mul_right: if G is a group with measurable multiplication, then right multiplication by g : G is a measurable automorphism of G;
• measurable_equiv.add_right: additive version of measurable_equiv.mul_right;
• measurable_equiv.mul_left₀, measurable_equiv.mul_right₀: versions of measurable_equiv.mul_left and measurable_equiv.mul_right for groups with zero;
• measurable_equiv.inv, measurable_equiv.inv₀: has_inv.inv as a measurable automorphism of a group (or a group with zero);
• measurable_equiv.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

def measurable_equiv.vadd {G : Type u_1} {α : Type u_3} [add_group G] [ α] [ α] (c : G) :
α ≃ᵐ α

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

Equations
@[simp]
theorem measurable_equiv.smul_to_equiv {G : Type u_1} {α : Type u_3} [group G] [ α] [ α] (c : G) :
def measurable_equiv.smul {G : Type u_1} {α : Type u_3} [group G] [ α] [ α] (c : G) :
α ≃ᵐ α

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

Equations
@[simp]
theorem measurable_equiv.smul_apply {G : Type u_1} {α : Type u_3} [group G] [ α] [ α] (c : G) :
@[simp]
theorem measurable_equiv.vadd_apply {G : Type u_1} {α : Type u_3} [add_group G] [ α] [ α] (c : G) :
@[simp]
theorem measurable_equiv.vadd_to_equiv {G : Type u_1} {α : Type u_3} [add_group G] [ α] [ α] (c : G) :
theorem measurable_embedding_const_vadd {G : Type u_1} {α : Type u_3} [add_group G] [ α] [ α] (c : G) :
theorem measurable_embedding_const_smul {G : Type u_1} {α : Type u_3} [group G] [ α] [ α] (c : G) :
@[simp]
theorem measurable_equiv.symm_vadd {G : Type u_1} {α : Type u_3} [add_group G] [ α] [ α] (c : G) :
@[simp]
theorem measurable_equiv.symm_smul {G : Type u_1} {α : Type u_3} [group G] [ α] [ α] (c : G) :
def measurable_equiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [group_with_zero 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
@[simp]
theorem measurable_equiv.coe_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [group_with_zero G₀] [ α] [ α] {c : G₀} (hc : c 0) :
@[simp]
theorem measurable_equiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [group_with_zero G₀] [ α] [ α] {c : G₀} (hc : c 0) :
theorem measurable_embedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [group_with_zero G₀] [ α] [ α] {c : G₀} (hc : c 0) :
def measurable_equiv.mul_left {G : Type u_1} [group 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
def measurable_equiv.add_left {G : Type u_1} [add_group G] (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
@[simp]
theorem measurable_equiv.coe_add_left {G : Type u_1} [add_group G] (g : G) :
@[simp]
theorem measurable_equiv.coe_mul_left {G : Type u_1} [group G] (g : G) :
@[simp]
theorem measurable_equiv.symm_add_left {G : Type u_1} [add_group G] (g : G) :
@[simp]
theorem measurable_equiv.symm_mul_left {G : Type u_1} [group G] (g : G) :
@[simp]
theorem measurable_equiv.to_equiv_mul_left {G : Type u_1} [group G] (g : G) :
@[simp]
theorem measurable_equiv.to_equiv_add_left {G : Type u_1} [add_group G] (g : G) :
theorem measurable_embedding_add_left {G : Type u_1} [add_group G] (g : G) :
theorem measurable_embedding_mul_left {G : Type u_1} [group G] (g : G) :
def measurable_equiv.mul_right {G : Type u_1} [group G] (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
def measurable_equiv.add_right {G : Type u_1} [add_group G] (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
theorem measurable_embedding_add_right {G : Type u_1} [add_group G] (g : G) :
measurable_embedding (λ (x : G), x + g)
theorem measurable_embedding_mul_right {G : Type u_1} [group G] (g : G) :
measurable_embedding (λ (x : G), x * g)
@[simp]
theorem measurable_equiv.coe_mul_right {G : Type u_1} [group G] (g : G) :
= λ (x : G), x * g
@[simp]
theorem measurable_equiv.coe_add_right {G : Type u_1} [add_group G] (g : G) :
= λ (x : G), x + g
@[simp]
theorem measurable_equiv.symm_mul_right {G : Type u_1} [group G] (g : G) :
@[simp]
theorem measurable_equiv.symm_add_right {G : Type u_1} [add_group G] (g : G) :
@[simp]
theorem measurable_equiv.to_equiv_add_right {G : Type u_1} [add_group G] (g : G) :
@[simp]
theorem measurable_equiv.to_equiv_mul_right {G : Type u_1} [group G] (g : G) :
def measurable_equiv.mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero 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
theorem measurable_embedding_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
@[simp]
theorem measurable_equiv.coe_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
@[simp]
theorem measurable_equiv.symm_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
@[simp]
theorem measurable_equiv.to_equiv_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
= hg
def measurable_equiv.mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero 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
theorem measurable_embedding_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
measurable_embedding (λ (x : G₀), x * g)
@[simp]
theorem measurable_equiv.coe_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
= λ (x : G₀), x * g
@[simp]
theorem measurable_equiv.symm_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
@[simp]
theorem measurable_equiv.to_equiv_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] {g : G₀} (hg : g 0) :
= hg
def measurable_equiv.inv (G : Type u_1) [group G]  :
G ≃ᵐ G

Inversion as a measurable automorphism of a group.

Equations
@[simp]
theorem measurable_equiv.inv_apply (G : Type u_1) [group G]  :
@[simp]
theorem measurable_equiv.inv_to_equiv (G : Type u_1) [group G]  :
def measurable_equiv.neg (G : Type u_1) [add_group G]  :
G ≃ᵐ G

Negation as a measurable automorphism of an additive group.

Equations
@[simp]
theorem measurable_equiv.neg_to_equiv (G : Type u_1) [add_group G]  :
@[simp]
theorem measurable_equiv.neg_apply (G : Type u_1) [add_group G]  :
@[simp]
theorem measurable_equiv.inv₀_apply (G₀ : Type u_2) [measurable_space G₀] [group_with_zero G₀]  :
@[simp]
theorem measurable_equiv.inv₀_to_equiv (G₀ : Type u_2) [measurable_space G₀] [group_with_zero G₀]  :
def measurable_equiv.inv₀ (G₀ : Type u_2) [measurable_space G₀] [group_with_zero G₀]  :
G₀ ≃ᵐ G₀

Inversion as a measurable automorphism of a group with zero.

Equations
@[simp]
theorem measurable_equiv.symm_inv {G : Type u_1} [group G]  :
@[simp]
theorem measurable_equiv.symm_inv₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀]  :