Measurability of Besicovitch's function

Each square wave is a step function, hence measurable, and g is a pointwise limit of finite sums of them.

theorem LeanPool.Besicovitch.Example.measurable_cellIndex (n : ℕ) : Measurable (cellIndex n)

theorem LeanPool.Besicovitch.Example.measurable_squareWave (n : ℕ) : Measurable (squareWave n)

theorem LeanPool.Besicovitch.Example.measurable_besicovitchFun : Measurable besicovitchFun