feat: Add measurable_abs (#9912)

See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/measurable_abs/near/417230631)



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib.lean

@@ -2698,7 +2698,6 @@ import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1
 import Mathlib.MeasureTheory.Integral.TorusIntegral
 import Mathlib.MeasureTheory.Integral.VitaliCaratheodory
-import Mathlib.MeasureTheory.Lattice
 import Mathlib.MeasureTheory.MeasurableSpace.Basic
 import Mathlib.MeasureTheory.MeasurableSpace.Card
 import Mathlib.MeasureTheory.MeasurableSpace.Defs
@@ -2747,6 +2746,8 @@ import Mathlib.MeasureTheory.Measure.Typeclasses
 import Mathlib.MeasureTheory.Measure.VectorMeasure
 import Mathlib.MeasureTheory.Measure.WithDensity
 import Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure
+import Mathlib.MeasureTheory.Order.Group.Lattice
+import Mathlib.MeasureTheory.Order.Lattice
 import Mathlib.MeasureTheory.PiSystem
 import Mathlib.MeasureTheory.SetSemiring
 import Mathlib.MeasureTheory.Tactic

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -6,9 +6,7 @@ Authors: Johannes Hölzl, Yury Kudryashov
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
 import Mathlib.MeasureTheory.Group.Arithmetic
-import Mathlib.MeasureTheory.Lattice
-import Mathlib.Topology.Algebra.Order.LiminfLimsup
-import Mathlib.Topology.ContinuousFunction.Basic
+import Mathlib.MeasureTheory.Order.Lattice
 import Mathlib.Topology.Instances.EReal
 import Mathlib.Topology.MetricSpace.HausdorffDistance
 import Mathlib.Topology.GDelta

Mathlib/MeasureTheory/Order/Group/Lattice.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import Mathlib.Algebra.Order.Group.PosPart
+import Mathlib.MeasureTheory.Group.Arithmetic
+import Mathlib.MeasureTheory.Order.Lattice
+
+
+/-!
+# Measurability results on groups with a lattice structure.
+
+## Tags
+
+measurable function, group, lattice operation
+-/
+
+variable {α β : Type*} [Lattice α] [Group α] [MeasurableSpace α]
+  [MeasurableSpace β] {f : β → α} (hf : Measurable f)
+
+variable [MeasurableSup α]
+
+@[to_additive (attr := measurability)]
+theorem measurable_oneLePart : Measurable (oneLePart : α → α) :=
+  measurable_sup_const _
+
+@[to_additive (attr := measurability)]
+protected theorem Measurable.oneLePart : Measurable fun x ↦ oneLePart (f x) :=
+  measurable_oneLePart.comp hf
+
+variable [MeasurableInv α]
+
+@[to_additive (attr := measurability)]
+theorem measurable_leOnePart : Measurable (leOnePart : α → α) :=
+  (measurable_sup_const _).comp measurable_inv
+
+@[to_additive (attr := measurability)]
+protected theorem Measurable.leOnePart : Measurable fun x ↦ leOnePart (f x) :=
+  measurable_leOnePart.comp hf
+
+variable [MeasurableSup₂ α]
+
+@[to_additive (attr := measurability)]
+theorem measurable_mabs : Measurable (mabs : α → α) :=
+  measurable_id'.sup measurable_inv
+
+@[to_additive (attr := measurability)]
+protected theorem Measurable.mabs : Measurable fun x ↦ mabs (f x) :=
+  measurable_mabs.comp hf