Measurability results on groups with a lattice structure. #
Tags #
measurable function, group, lattice operation
theorem
measurable_oneLePart
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[DivInvMonoid α]
[MeasurableSup α]
:
theorem
measurable_posPart
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[SubNegMonoid α]
[MeasurableSup α]
:
theorem
Measurable.oneLePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
(hf : Measurable f)
:
theorem
Measurable.fun_oneLePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
(hf : Measurable f)
:
Measurable fun (i : β) => (f i)⁺ᵐ
Eta-expanded form of Measurable.oneLePart
theorem
Measurable.fun_posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
(hf : Measurable f)
:
Measurable fun (i : β) => (f i)⁺
theorem
Measurable.posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
(hf : Measurable f)
:
theorem
AEMeasurable.oneLePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable f⁺ᵐ μ
theorem
AEMeasurable.fun_oneLePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (i : β) => (f i)⁺ᵐ) μ
Eta-expanded form of AEMeasurable.oneLePart
theorem
AEMeasurable.fun_posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (i : β) => (f i)⁺) μ
theorem
AEMeasurable.posPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable f⁺ μ
theorem
measurable_leOnePart
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[DivInvMonoid α]
[MeasurableSup α]
[MeasurableInv α]
:
theorem
measurable_negPart
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[SubNegMonoid α]
[MeasurableSup α]
[MeasurableNeg α]
:
theorem
Measurable.leOnePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
[MeasurableInv α]
(hf : Measurable f)
:
theorem
Measurable.fun_leOnePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
[MeasurableInv α]
(hf : Measurable f)
:
Measurable fun (i : β) => (f i)⁻ᵐ
Eta-expanded form of Measurable.leOnePart
theorem
Measurable.fun_negPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
[MeasurableNeg α]
(hf : Measurable f)
:
Measurable fun (i : β) => (f i)⁻
theorem
Measurable.negPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
[MeasurableNeg α]
(hf : Measurable f)
:
theorem
AEMeasurable.leOnePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
[MeasurableInv α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable f⁻ᵐ μ
theorem
AEMeasurable.fun_leOnePart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[DivInvMonoid α]
[MeasurableSup α]
[MeasurableInv α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (i : β) => (f i)⁻ᵐ) μ
Eta-expanded form of AEMeasurable.leOnePart
theorem
AEMeasurable.negPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
[MeasurableNeg α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable f⁻ μ
theorem
AEMeasurable.fun_negPart
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[SubNegMonoid α]
[MeasurableSup α]
[MeasurableNeg α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (i : β) => (f i)⁻) μ
theorem
measurable_mabs
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[Group α]
[MeasurableInv α]
[MeasurableSup₂ α]
:
theorem
measurable_abs
{α : Type u_1}
[Lattice α]
[MeasurableSpace α]
[AddGroup α]
[MeasurableNeg α]
[MeasurableSup₂ α]
:
theorem
Measurable.mabs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[Group α]
[MeasurableInv α]
[MeasurableSup₂ α]
(hf : Measurable f)
:
Measurable fun (x : β) => |f x|ₘ
theorem
Measurable.abs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[AddGroup α]
[MeasurableNeg α]
[MeasurableSup₂ α]
(hf : Measurable f)
:
Measurable fun (x : β) => |f x|
theorem
AEMeasurable.mabs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[Group α]
[MeasurableInv α]
[MeasurableSup₂ α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : β) => |f x|ₘ) μ
theorem
AEMeasurable.abs
{α : Type u_1}
{β : Type u_2}
[Lattice α]
[MeasurableSpace α]
[MeasurableSpace β]
{f : β → α}
[AddGroup α]
[MeasurableNeg α]
[MeasurableSup₂ α]
{μ : MeasureTheory.Measure β}
(hf : AEMeasurable f μ)
:
AEMeasurable (fun (x : β) => |f x|) μ