# Documentation

Mathlib.MeasureTheory.Group.MeasurableEquiv

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

Instances For
theorem MeasurableEquiv.vadd.proof_2 {G : Type u_2} {α : Type u_1} [] [] [] [] [] (c : G) :
Measurable ((fun x x_1 => x +ᵥ x_1) (-c))
@[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 α.

Instances For
theorem measurableEmbedding_const_vadd {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
MeasurableEmbedding ((fun x x_1 => x +ᵥ x_1) c)
theorem measurableEmbedding_const_smul {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
MeasurableEmbedding ((fun x x_1 => x x_1) c)
@[simp]
theorem MeasurableEquiv.symm_vadd {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
@[simp]
theorem MeasurableEquiv.symm_smul {G : Type u_1} {α : Type u_3} [] [] [] [] [] (c : G) :
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 α

Instances For
@[simp]
theorem MeasurableEquiv.coe_smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
↑() = (fun x x_1 => x x_1) c
@[simp]
theorem MeasurableEquiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
theorem measurableEmbedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [] [] [] [MulAction G₀ α] [] {c : G₀} (hc : c 0) :
MeasurableEmbedding ((fun x x_1 => x x_1) c)
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.

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.

Instances For
@[simp]
theorem MeasurableEquiv.coe_addLeft {G : Type u_1} [] [] [] (g : G) :
= (fun x x_1 => x + x_1) g
@[simp]
theorem MeasurableEquiv.coe_mulLeft {G : Type u_1} [] [] [] (g : G) :
= (fun x x_1 => x * x_1) g
@[simp]
theorem MeasurableEquiv.symm_addLeft {G : Type u_1} [] [] [] (g : G) :
@[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 x_1 => x + x_1) g)
theorem measurableEmbedding_mulLeft {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding ((fun x x_1 => x * x_1) g)
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.

Instances For
theorem MeasurableEquiv.addRight.proof_1 {G : Type u_1} [] [] [] (g : G) :
Measurable fun x => x + g
theorem MeasurableEquiv.addRight.proof_2 {G : Type u_1} [] [] [] (g : G) :
Measurable fun x => 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.

Instances For
theorem measurableEmbedding_addRight {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun x => x + g
theorem measurableEmbedding_mulRight {G : Type u_1} [] [] [] (g : G) :
MeasurableEmbedding fun x => x * g
@[simp]
theorem MeasurableEquiv.coe_addRight {G : Type u_1} [] [] [] (g : G) :
= fun x => x + g
@[simp]
theorem MeasurableEquiv.coe_mulRight {G : Type u_1} [] [] [] (g : G) :
= fun x => x * g
@[simp]
theorem MeasurableEquiv.symm_addRight {G : Type u_1} [] [] [] (g : G) :
@[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₀.

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

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

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.

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

equiv.subRight as a MeasurableEquiv

Instances For
def MeasurableEquiv.divRight {G : Type u_1} [] [] [] (g : G) :
G ≃ᵐ G

equiv.divRight as a MeasurableEquiv.

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

equiv.subLeft as a MeasurableEquiv

Instances For
def MeasurableEquiv.divLeft {G : Type u_1} [] [] [] [] (g : G) :
G ≃ᵐ G

equiv.divLeft as a MeasurableEquiv

Instances For