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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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: 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} [measurable_space G] [measurable_space α] [add_group G] [add_action G α] [has_measurable_vadd G α] (c : G) :

α ≃ᵐ α

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

Equations

measurable_equiv.vadd c = {to_equiv := add_action.to_perm c, measurable_to_fun := _, measurable_inv_fun := _}

source

@[simp]

theorem measurable_equiv.smul_to_equiv {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (c : G) :

(measurable_equiv.smul c).to_equiv = mul_action.to_perm c

source

def measurable_equiv.smul {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (c : G) :

α ≃ᵐ α

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

Equations

measurable_equiv.smul c = {to_equiv := mul_action.to_perm c, measurable_to_fun := _, measurable_inv_fun := _}

source

@[simp]

theorem measurable_equiv.smul_apply {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (c : G) :

⇑(measurable_equiv.smul c) = has_smul.smul c

source

@[simp]

theorem measurable_equiv.vadd_apply {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [add_group G] [add_action G α] [has_measurable_vadd G α] (c : G) :

⇑(measurable_equiv.vadd c) = has_vadd.vadd c

source

@[simp]

theorem measurable_equiv.vadd_to_equiv {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [add_group G] [add_action G α] [has_measurable_vadd G α] (c : G) :

(measurable_equiv.vadd c).to_equiv = add_action.to_perm c

source

theorem measurable_embedding_const_vadd {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [add_group G] [add_action G α] [has_measurable_vadd G α] (c : G) :

measurable_embedding (has_vadd.vadd c)

source

theorem measurable_embedding_const_smul {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (c : G) :

measurable_embedding (has_smul.smul c)

source

@[simp]

theorem measurable_equiv.symm_vadd {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [add_group G] [add_action G α] [has_measurable_vadd G α] (c : G) :

(measurable_equiv.vadd c).symm = measurable_equiv.vadd (-c)

source

@[simp]

theorem measurable_equiv.symm_smul {G : Type u_1} {α : Type u_3} [measurable_space G] [measurable_space α] [group G] [mul_action G α] [has_measurable_smul G α] (c : G) :

(measurable_equiv.smul c).symm = measurable_equiv.smul c⁻¹

source

def measurable_equiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [measurable_space α] [group_with_zero G₀] [mul_action G₀ α] [has_measurable_smul 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

measurable_equiv.smul₀ c hc = measurable_equiv.smul (units.mk0 c hc)

source

@[simp]

theorem measurable_equiv.coe_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [measurable_space α] [group_with_zero G₀] [mul_action G₀ α] [has_measurable_smul G₀ α] {c : G₀} (hc : c ≠ 0) :

⇑(measurable_equiv.smul₀ c hc) = has_smul.smul c

source

@[simp]

theorem measurable_equiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [measurable_space α] [group_with_zero G₀] [mul_action G₀ α] [has_measurable_smul G₀ α] {c : G₀} (hc : c ≠ 0) :

(measurable_equiv.smul₀ c hc).symm = measurable_equiv.smul₀ c⁻¹ _

source

theorem measurable_embedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [measurable_space G₀] [measurable_space α] [group_with_zero G₀] [mul_action G₀ α] [has_measurable_smul G₀ α] {c : G₀} (hc : c ≠ 0) :

measurable_embedding (has_smul.smul c)

source

def measurable_equiv.mul_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul 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

measurable_equiv.mul_left g = measurable_equiv.smul g

source

def measurable_equiv.add_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add 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

measurable_equiv.add_left g = measurable_equiv.vadd g

source

@[simp]

theorem measurable_equiv.coe_add_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

⇑(measurable_equiv.add_left g) = has_add.add g

source

@[simp]

theorem measurable_equiv.coe_mul_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

⇑(measurable_equiv.mul_left g) = has_mul.mul g

source

@[simp]

theorem measurable_equiv.symm_add_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

(measurable_equiv.add_left g).symm = measurable_equiv.add_left (-g)

source

@[simp]

theorem measurable_equiv.symm_mul_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

(measurable_equiv.mul_left g).symm = measurable_equiv.mul_left g⁻¹

source

@[simp]

theorem measurable_equiv.to_equiv_mul_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

(measurable_equiv.mul_left g).to_equiv = equiv.mul_left g

source

@[simp]

theorem measurable_equiv.to_equiv_add_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

(measurable_equiv.add_left g).to_equiv = equiv.add_left g

source

theorem measurable_embedding_add_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

measurable_embedding (has_add.add g)

source

theorem measurable_embedding_mul_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

measurable_embedding (has_mul.mul g)

source

def measurable_equiv.mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul 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

measurable_equiv.mul_right g = {to_equiv := equiv.mul_right g, measurable_to_fun := _, measurable_inv_fun := _}

source

def measurable_equiv.add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add 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

measurable_equiv.add_right g = {to_equiv := equiv.add_right g, measurable_to_fun := _, measurable_inv_fun := _}

source

theorem measurable_embedding_add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

measurable_embedding (λ (x : G), x + g)

source

theorem measurable_embedding_mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

measurable_embedding (λ (x : G), x * g)

source

@[simp]

theorem measurable_equiv.coe_mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

⇑(measurable_equiv.mul_right g) = λ (x : G), x * g

source

@[simp]

theorem measurable_equiv.coe_add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

⇑(measurable_equiv.add_right g) = λ (x : G), x + g

source

@[simp]

theorem measurable_equiv.symm_mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

(measurable_equiv.mul_right g).symm = measurable_equiv.mul_right g⁻¹

source

@[simp]

theorem measurable_equiv.symm_add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

(measurable_equiv.add_right g).symm = measurable_equiv.add_right (-g)

source

@[simp]

theorem measurable_equiv.to_equiv_add_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

(measurable_equiv.add_right g).to_equiv = equiv.add_right g

source

@[simp]

theorem measurable_equiv.to_equiv_mul_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

(measurable_equiv.mul_right g).to_equiv = equiv.mul_right g

source

def measurable_equiv.mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul 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

measurable_equiv.mul_left₀ g hg = measurable_equiv.smul₀ g hg

source

theorem measurable_embedding_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

measurable_embedding (has_mul.mul g)

source

@[simp]

theorem measurable_equiv.coe_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

⇑(measurable_equiv.mul_left₀ g hg) = has_mul.mul g

source

@[simp]

theorem measurable_equiv.symm_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

(measurable_equiv.mul_left₀ g hg).symm = measurable_equiv.mul_left₀ g⁻¹ _

source

@[simp]

theorem measurable_equiv.to_equiv_mul_left₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

(measurable_equiv.mul_left₀ g hg).to_equiv = equiv.mul_left₀ g hg

source

def measurable_equiv.mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul 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

measurable_equiv.mul_right₀ g hg = {to_equiv := equiv.mul_right₀ g hg, measurable_to_fun := _, measurable_inv_fun := _}

source

theorem measurable_embedding_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

measurable_embedding (λ (x : G₀), x * g)

source

@[simp]

theorem measurable_equiv.coe_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

⇑(measurable_equiv.mul_right₀ g hg) = λ (x : G₀), x * g

source

@[simp]

theorem measurable_equiv.symm_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

(measurable_equiv.mul_right₀ g hg).symm = measurable_equiv.mul_right₀ g⁻¹ _

source

@[simp]

theorem measurable_equiv.to_equiv_mul_right₀ {G₀ : Type u_2} [measurable_space G₀] [group_with_zero G₀] [has_measurable_mul G₀] {g : G₀} (hg : g ≠ 0) :

(measurable_equiv.mul_right₀ g hg).to_equiv = equiv.mul_right₀ g hg

source

def measurable_equiv.inv (G : Type u_1) [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :

G ≃ᵐ G

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

Equations

measurable_equiv.inv G = {to_equiv := equiv.inv G _inst_11, measurable_to_fun := _, measurable_inv_fun := _}

source

@[simp]

theorem measurable_equiv.inv_apply (G : Type u_1) [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :

⇑(measurable_equiv.inv G) = has_inv.inv

source

@[simp]

theorem measurable_equiv.inv_to_equiv (G : Type u_1) [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :

(measurable_equiv.inv G).to_equiv = equiv.inv G

source

def measurable_equiv.neg (G : Type u_1) [measurable_space G] [has_involutive_neg G] [has_measurable_neg G] :

G ≃ᵐ G

Negation as a measurable automorphism of an additive group.

Equations

measurable_equiv.neg G = {to_equiv := equiv.neg G _inst_11, measurable_to_fun := _, measurable_inv_fun := _}

source

@[simp]

theorem measurable_equiv.neg_to_equiv (G : Type u_1) [measurable_space G] [has_involutive_neg G] [has_measurable_neg G] :

(measurable_equiv.neg G).to_equiv = equiv.neg G

source

@[simp]

theorem measurable_equiv.neg_apply (G : Type u_1) [measurable_space G] [has_involutive_neg G] [has_measurable_neg G] :

⇑(measurable_equiv.neg G) = has_neg.neg

source

@[simp]

theorem measurable_equiv.symm_inv {G : Type u_1} [measurable_space G] [has_involutive_inv G] [has_measurable_inv G] :

(measurable_equiv.inv G).symm = measurable_equiv.inv G

source

@[simp]

theorem measurable_equiv.symm_neg {G : Type u_1} [measurable_space G] [has_involutive_neg G] [has_measurable_neg G] :

(measurable_equiv.neg G).symm = measurable_equiv.neg G

source

def measurable_equiv.div_right {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] (g : G) :

G ≃ᵐ G

equiv.div_right as a measurable_equiv.

Equations

measurable_equiv.div_right g = {to_equiv := equiv.div_right g, measurable_to_fun := _, measurable_inv_fun := _}

source

def measurable_equiv.sub_right {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] (g : G) :

G ≃ᵐ G

equiv.sub_right as a measurable_equiv

Equations

measurable_equiv.sub_right g = {to_equiv := equiv.sub_right g, measurable_to_fun := _, measurable_inv_fun := _}

source

def measurable_equiv.div_left {G : Type u_1} [measurable_space G] [group G] [has_measurable_mul G] [has_measurable_inv G] (g : G) :

G ≃ᵐ G

equiv.div_left as a measurable_equiv

Equations

measurable_equiv.div_left g = {to_equiv := equiv.div_left g, measurable_to_fun := _, measurable_inv_fun := _}

source

def measurable_equiv.sub_left {G : Type u_1} [measurable_space G] [add_group G] [has_measurable_add G] [has_measurable_neg G] (g : G) :

G ≃ᵐ G

equiv.sub_left as a measurable_equiv

Equations

measurable_equiv.sub_left g = {to_equiv := equiv.sub_left g, measurable_to_fun := _, measurable_inv_fun := _}