Measurability results on groups with a lattice structure.

Tags

measurable function, group, lattice operation

theorem measurable_oneLePart {α : Type u_1} [Lattice α] [MeasurableSpace α] [DivInvMonoid α] [MeasurableSup α] : Measurable oneLePart

theorem measurable_posPart {α : Type u_1} [Lattice α] [MeasurableSpace α] [SubNegMonoid α] [MeasurableSup α] : Measurable posPart

theorem Measurable.oneLePart {α : Type u_1} {β : Type u_2} [Lattice α] [MeasurableSpace α] [MeasurableSpace β] {f : β → α} [DivInvMonoid α] [MeasurableSup α] (hf : Measurable f) : 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) : 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 α] : Measurable leOnePart

theorem measurable_negPart {α : Type u_1} [Lattice α] [MeasurableSpace α] [SubNegMonoid α] [MeasurableSup α] [MeasurableNeg α] : Measurable negPart

theorem Measurable.leOnePart {α : Type u_1} {β : Type u_2} [Lattice α] [MeasurableSpace α] [MeasurableSpace β] {f : β → α} [DivInvMonoid α] [MeasurableSup α] [MeasurableInv α] (hf : Measurable f) : 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) : 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₂ α] : Measurable mabs

theorem measurable_abs {α : Type u_1} [Lattice α] [MeasurableSpace α] [AddGroup α] [MeasurableNeg α] [MeasurableSup₂ α] : Measurable abs

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|) μ