(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

def MeasurableEquiv.smul {G : Type u_1} {α : Type u_3} [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableConstSMul 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_invFun := ⋯ }

def MeasurableEquiv.vadd {G : Type u_1} {α : Type u_3} [MeasurableSpace α] [AddGroup G] [AddAction G α] [MeasurableConstVAdd 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_invFun := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

def MeasurableEquiv.smul₀ {G₀ : Type u_2} {α : Type u_3} [MeasurableSpace α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableConstSMul 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 α] [GroupWithZero G₀] [MulAction G₀ α] [MeasurableConstSMul G₀ α] {c : G₀} (hc : c ≠ 0) : ⇑(smul₀ c hc) = fun (x : α) => c • x

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def MeasurableEquiv.mulLeft₀ {G₀ : Type u_2} [GroupWithZero G₀] [MeasurableSpace 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} [GroupWithZero G₀] [MeasurableSpace G₀] [MeasurableMul G₀] {g : G₀} (hg : g ≠ 0) : MeasurableEmbedding fun (x : G₀) => g * x

@[simp]

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

@[simp]

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

@[simp]

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

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

• MeasurableEquiv.mulRight₀ g hg = { toEquiv := Equiv.mulRight₀ g hg, measurable_toFun := ⋯, measurable_invFun := ⋯ }

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

@[simp]

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

@[simp]

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

@[simp]

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

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_invFun := ⋯ }

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_invFun := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

equiv.divRight as a MeasurableEquiv.

Equations

• MeasurableEquiv.divRight g = { toEquiv := Equiv.divRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

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

equiv.subRight as a MeasurableEquiv

Equations

• MeasurableEquiv.subRight g = { toEquiv := Equiv.subRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }

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

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

def MeasurableEquiv.divLeft {G : Type u_1} [Group G] [MeasurableSpace 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_invFun := ⋯ }

def MeasurableEquiv.subLeft {G : Type u_1} [AddGroup G] [MeasurableSpace 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_invFun := ⋯ }

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

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

noncomputable instance MeasureTheory.Measure.instDistribMulActionDomMulAct {G : Type u_1} {A : Type u_2} [Group G] [MulAction G A] [MeasurableSpace A] [MeasurableConstSMul G A] : DistribMulAction Gᵈᵐᵃ (Measure A)

Equations

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

theorem MeasureTheory.Measure.domSMul_apply {G : Type u_1} {A : Type u_2} [Group G] [MulAction G A] [MeasurableSpace A] [MeasurableConstSMul G A] (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) : (g • μ) s = μ (DomMulAct.mk.symm g • s)

@[deprecated MeasureTheory.Measure.domSMul_apply (since := "2025-08-05")]

theorem MeasureTheory.Measure.dmaSMul_apply {G : Type u_1} {A : Type u_2} [Group G] [MulAction G A] [MeasurableSpace A] [MeasurableConstSMul G A] (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) : (g • μ) s = μ (DomMulAct.mk.symm g • s)

Alias of MeasureTheory.Measure.domSMul_apply.

instance MeasureTheory.Measure.instSMulCommClassNNRealDomMulAct {G : Type u_1} {A : Type u_2} [Group G] [MulAction G A] [MeasurableSpace A] [MeasurableConstSMul G A] : SMulCommClass NNReal Gᵈᵐᵃ (Measure A)

instance MeasureTheory.Measure.instSMulCommClassDomMulActNNReal {G : Type u_1} {A : Type u_2} [Group G] [MulAction G A] [MeasurableSpace A] [MeasurableConstSMul G A] : SMulCommClass Gᵈᵐᵃ NNReal (Measure A)