measurable_abs

Stream: Is there code for X?

[Xavier Roblot]

We don't seem to have the fact that abs is measurable (eg. for the reals). It is not difficult to prove, see

import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

variable {R : Type*} [TopologicalSpace R] [LinearOrderedRing R] [TopologicalRing R]
  [MeasurableSpace R] [MeasurableNeg R] [OpensMeasurableSpace R] [OrderClosedTopology R]
  [SecondCountableTopology R]

theorem measurable_abs : Measurable fun x : R ↦ |x| := Measurable.max measurable_id' measurable_neg

I am not sure about the hypotheses though since I just added everything that Lean was complaining about :wink:

[Yaël Dillies]

You should just need MeasurableSup₂ and MeasurableNeg (and you can multiplicativise it.

[Xavier Roblot]

Ok, so this is the latest version:

import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

variable {R : Type*} [Lattice R] [Group R] [MeasurableSpace R] [MeasurableSup₂ R]
  [MeasurableInv R]

@[to_additive (attr := measurability)]
theorem measurable_mabs : Measurable fun x : R ↦ mabs x :=
  Measurable.sup measurable_id' measurable_inv

But, now, I don't know where to put it since the first file to contain all the necessary imports is Mathlib.MeasureTheory.Constructions.BorelSpace.Basic and it's already quite large and does not look like a good fit.

[Eric Rodriguez]

new files are cheap!

[Xavier Roblot]

I always feel bad about making a new file to put so little...

[Yaël Dillies]

Put it where MeasurableSup₂ is defined.

[Xavier Roblot]

Yaël Dillies said:

Put it where MeasurableSup₂ is defined.

MeasurableInv is unknown there...

[Yaël Dillies]

Then create MeasureTheory.Order.Group.Lattice

[Yaël Dillies]

... and move MeasureTheory.Lattice to MeasureTheory.Order.Lattice

[Xavier Roblot]

#9912