mathlib documentation

measure_theory.group.measurable_equiv

(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

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
@[simp]
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
@[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) :
@[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) :
@[simp]
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) :
@[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) :
@[simp]
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
@[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) :
@[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) :
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) :
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
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
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
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
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)
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)
@[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
@[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
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
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) :
@[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) :
@[simp]
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
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)
@[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
@[simp]

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

Equations

Negation as a measurable automorphism of an additive group.

Equations