(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} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : Measurable fun (x : α) => c +ᵥ x

def MeasurableEquiv.vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : α ≃ᵐ α

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

Equations

• MeasurableEquiv.vadd c = { toEquiv := AddAction.toPerm c, measurable_toFun := (_ : Measurable fun (x : α) => c +ᵥ x), measurable_invFun := (_ : Measurable fun (x : α) => -c +ᵥ x) }

theorem MeasurableEquiv.vadd.proof_2 {G : Type u_2} {α : Type u_1} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : Measurable fun (x : α) => -c +ᵥ x

@[simp]

theorem MeasurableEquiv.vadd_apply {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : ⇑(MeasurableEquiv.vadd c) = fun (x : α) => c +ᵥ x

@[simp]

theorem MeasurableEquiv.vadd_toEquiv {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : (MeasurableEquiv.vadd c).toEquiv = AddAction.toPerm c

@[simp]

theorem MeasurableEquiv.smul_apply {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) : ⇑(MeasurableEquiv.smul c) = fun (x : α) => c • x

@[simp]

theorem MeasurableEquiv.smul_toEquiv {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) : (MeasurableEquiv.smul c).toEquiv = MulAction.toPerm c

def MeasurableEquiv.smul {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) : α ≃ᵐ α

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

Equations

• MeasurableEquiv.smul c = { toEquiv := MulAction.toPerm c, measurable_toFun := (_ : Measurable fun (x : α) => c • x), measurable_invFun := (_ : Measurable fun (x : α) => c⁻¹ • x) }

theorem measurableEmbedding_const_vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : MeasurableEmbedding fun (x : α) => c +ᵥ x

theorem measurableEmbedding_const_smul {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) : MeasurableEmbedding fun (x : α) => c • x

@[simp]

theorem MeasurableEquiv.symm_vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableVAdd G α] (c : G) : (MeasurableEquiv.vadd c).symm = MeasurableEquiv.vadd (-c)

@[simp]

theorem MeasurableEquiv.symm_smul {G : Type u_1} {α : Type u_3} [MeasurableSpace G] [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableSMul G α] (c : G) : (MeasurableEquiv.smul c).symm = MeasurableEquiv.smul c⁻¹

def MeasurableEquiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul 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

• MeasurableEquiv.smul₀ c hc = MeasurableEquiv.smul (Units.mk0 c hc)

@[simp]

theorem MeasurableEquiv.coe_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c ≠ 0) : ⇑(MeasurableEquiv.smul₀ c hc) = fun (x : α) => c • x

@[simp]

theorem MeasurableEquiv.symm_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c ≠ 0) : (MeasurableEquiv.smul₀ c hc).symm = MeasurableEquiv.smul₀ c⁻¹ (_ : c⁻¹ ≠ 0)

theorem measurableEmbedding_const_smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace G₀] [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableSMul G₀ α] {c : G₀} (hc : c ≠ 0) : MeasurableEmbedding fun (x : α) => c • x

theorem MeasurableEquiv.addLeft.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] : MeasurableVAdd G G

def MeasurableEquiv.addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd 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

• MeasurableEquiv.addLeft g = MeasurableEquiv.vadd g

def MeasurableEquiv.mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul 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

• MeasurableEquiv.mulLeft g = MeasurableEquiv.smul g

@[simp]

theorem MeasurableEquiv.coe_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : ⇑(MeasurableEquiv.addLeft g) = fun (x : G) => g + x

@[simp]

theorem MeasurableEquiv.coe_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : ⇑(MeasurableEquiv.mulLeft g) = fun (x : G) => g * x

@[simp]

theorem MeasurableEquiv.symm_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : (MeasurableEquiv.addLeft g).symm = MeasurableEquiv.addLeft (-g)

@[simp]

theorem MeasurableEquiv.symm_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : (MeasurableEquiv.mulLeft g).symm = MeasurableEquiv.mulLeft g⁻¹

@[simp]

theorem MeasurableEquiv.toEquiv_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : (MeasurableEquiv.addLeft g).toEquiv = Equiv.addLeft g

@[simp]

theorem MeasurableEquiv.toEquiv_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : (MeasurableEquiv.mulLeft g).toEquiv = Equiv.mulLeft g

theorem measurableEmbedding_addLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : MeasurableEmbedding fun (x : G) => g + x

theorem measurableEmbedding_mulLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : MeasurableEmbedding fun (x : G) => g * x

def MeasurableEquiv.addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd 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

• MeasurableEquiv.addRight g = { toEquiv := Equiv.addRight g, measurable_toFun := (_ : Measurable fun (x : G) => x + g), measurable_invFun := (_ : Measurable fun (x : G) => x + -g) }

theorem MeasurableEquiv.addRight.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : Measurable fun (x : G) => x + g

theorem MeasurableEquiv.addRight.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : Measurable fun (x : G) => x + -g

def MeasurableEquiv.mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul 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

• MeasurableEquiv.mulRight g = { toEquiv := Equiv.mulRight g, measurable_toFun := (_ : Measurable fun (x : G) => x * g), measurable_invFun := (_ : Measurable fun (x : G) => x * g⁻¹) }

theorem measurableEmbedding_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : MeasurableEmbedding fun (x : G) => x + g

theorem measurableEmbedding_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : MeasurableEmbedding fun (x : G) => x * g

@[simp]

theorem MeasurableEquiv.coe_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : ⇑(MeasurableEquiv.addRight g) = fun (x : G) => x + g

@[simp]

theorem MeasurableEquiv.coe_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : ⇑(MeasurableEquiv.mulRight g) = fun (x : G) => x * g

@[simp]

theorem MeasurableEquiv.symm_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : (MeasurableEquiv.addRight g).symm = MeasurableEquiv.addRight (-g)

@[simp]

theorem MeasurableEquiv.symm_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : (MeasurableEquiv.mulRight g).symm = MeasurableEquiv.mulRight g⁻¹

@[simp]

theorem MeasurableEquiv.toEquiv_addRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : (MeasurableEquiv.addRight g).toEquiv = Equiv.addRight g

@[simp]

theorem MeasurableEquiv.toEquiv_mulRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : (MeasurableEquiv.mulRight g).toEquiv = Equiv.mulRight g

def MeasurableEquiv.mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul 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

• MeasurableEquiv.mulLeft₀ g hg = MeasurableEquiv.smul₀ g hg

theorem measurableEmbedding_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : MeasurableEmbedding fun (x : G₀) => g * x

@[simp]

theorem MeasurableEquiv.coe_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : ⇑(MeasurableEquiv.mulLeft₀ g hg) = fun (x : G₀) => g * x

@[simp]

theorem MeasurableEquiv.symm_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : (MeasurableEquiv.mulLeft₀ g hg).symm = MeasurableEquiv.mulLeft₀ g⁻¹ (_ : g⁻¹ ≠ 0)

@[simp]

theorem MeasurableEquiv.toEquiv_mulLeft₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : (MeasurableEquiv.mulLeft₀ g hg).toEquiv = Equiv.mulLeft₀ g hg

def MeasurableEquiv.mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul 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

• One or more equations did not get rendered due to their size.

theorem measurableEmbedding_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : MeasurableEmbedding fun (x : G₀) => x * g

@[simp]

theorem MeasurableEquiv.coe_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : ⇑(MeasurableEquiv.mulRight₀ g hg) = fun (x : G₀) => x * g

@[simp]

theorem MeasurableEquiv.symm_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : (MeasurableEquiv.mulRight₀ g hg).symm = MeasurableEquiv.mulRight₀ g⁻¹ (_ : g⁻¹ ≠ 0)

@[simp]

theorem MeasurableEquiv.toEquiv_mulRight₀ {G₀ : Type u_2} [MeasurableSpace G₀] [GroupWithZero G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : (MeasurableEquiv.mulRight₀ g hg).toEquiv = Equiv.mulRight₀ g hg

def MeasurableEquiv.neg (G : Type u_4) [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] : G ≃ᵐ G

Negation as a measurable automorphism of an additive group.

Equations

• MeasurableEquiv.neg G = { toEquiv := Equiv.neg G, measurable_toFun := (_ : Measurable Neg.neg), measurable_invFun := (_ : Measurable Neg.neg) }

theorem MeasurableEquiv.neg.proof_1 (G : Type u_1) [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] : Measurable Neg.neg

@[simp]

theorem MeasurableEquiv.neg_toEquiv (G : Type u_4) [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] : (MeasurableEquiv.neg G).toEquiv = Equiv.neg G

@[simp]

theorem MeasurableEquiv.inv_toEquiv (G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : (MeasurableEquiv.inv G).toEquiv = Equiv.inv G

@[simp]

theorem MeasurableEquiv.inv_apply (G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : ⇑(MeasurableEquiv.inv G) = Inv.inv

@[simp]

theorem MeasurableEquiv.neg_apply (G : Type u_4) [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] : ⇑(MeasurableEquiv.neg G) = Neg.neg

def MeasurableEquiv.inv (G : Type u_4) [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : G ≃ᵐ G

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

Equations

• MeasurableEquiv.inv G = { toEquiv := Equiv.inv G, measurable_toFun := (_ : Measurable Inv.inv), measurable_invFun := (_ : Measurable Inv.inv) }

@[simp]

theorem MeasurableEquiv.symm_neg {G : Type u_4} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] : (MeasurableEquiv.neg G).symm = MeasurableEquiv.neg G

@[simp]

theorem MeasurableEquiv.symm_inv {G : Type u_4} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] : (MeasurableEquiv.inv G).symm = MeasurableEquiv.inv G

theorem MeasurableEquiv.subRight.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : Measurable fun (x : G) => x + g

theorem MeasurableEquiv.subRight.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : Measurable fun (h : G) => h - g

def MeasurableEquiv.subRight {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (g : G) : G ≃ᵐ G

equiv.subRight as a MeasurableEquiv

Equations

• MeasurableEquiv.subRight g = { toEquiv := Equiv.subRight g, measurable_toFun := (_ : Measurable fun (h : G) => h - g), measurable_invFun := (_ : Measurable fun (x : G) => x + g) }

def MeasurableEquiv.divRight {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] (g : G) : G ≃ᵐ G

equiv.divRight as a MeasurableEquiv.

Equations

• MeasurableEquiv.divRight g = { toEquiv := Equiv.divRight g, measurable_toFun := (_ : Measurable fun (h : G) => h / g), measurable_invFun := (_ : Measurable fun (x : G) => x * g) }

theorem MeasurableEquiv.subLeft.proof_2 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (g : G) : Measurable fun (x : G) => -x + g

theorem MeasurableEquiv.subLeft.proof_1 {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (g : G) : Measurable fun (x : G) => g - id x

def MeasurableEquiv.subLeft {G : Type u_1} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (g : G) : G ≃ᵐ G

equiv.subLeft as a MeasurableEquiv

Equations

• MeasurableEquiv.subLeft g = { toEquiv := Equiv.subLeft g, measurable_toFun := (_ : Measurable fun (x : G) => g - id x), measurable_invFun := (_ : Measurable fun (x : G) => -x + g) }

def MeasurableEquiv.divLeft {G : Type u_1} [MeasurableSpace G] [Group G] [MeasurableMul G] [MeasurableInv G] (g : G) : G ≃ᵐ G

equiv.divLeft as a MeasurableEquiv

Equations

• MeasurableEquiv.divLeft g = { toEquiv := Equiv.divLeft g, measurable_toFun := (_ : Measurable fun (x : G) => g / id x), measurable_invFun := (_ : Measurable fun (x : G) => x⁻¹ * g) }