Measurability of Monotone/Right Continuous functions

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

I am pretty sure we don't have the following, but just to double check...

import Mathlib

open MeasureTheory

variable {f : ℝ → ℝ}

theorem RightContinuous.aestronglyMeasurable (hf : ∀ x, ContinuousWithinAt f (Set.Ici x) x) :
    AEStronglyMeasurable f := by
  sorry

theorem Monotone.aestronglyMeasurable (hf : Monotone f) :
    AEStronglyMeasurable f := by
  sorry

theorem countable_discontinuities_aestronglyMeasurable (hf : Set.Countable {x | ¬ContinuousAt f x}) :
    AEStronglyMeasurable f := by
  sorry

[Rémy Degenne]

A proof of the second one:

import Mathlib

open MeasureTheory

variable {f : ℝ → ℝ}

theorem Monotone.aestronglyMeasurable (hf : Monotone f) :
    AEStronglyMeasurable f :=
  hf.measurable.aestronglyMeasurable

[Yongxi Lin (Aaron)]

oh yeah on R they are the same!

[Ruben Van de Velde]

Does docs#ContinuousOn.aestronglyMeasurable help?

[Yongxi Lin (Aaron)]

@Ruben Van de Velde
Yes and this will be related to one of my draft PRs #33586. I am planning to prove that right continuous function is continuous with respect to the lower limit topology in this PR, and then one can take advantage of ContinuousOn.aestronglyMeasurable