MeasureTheory.set_integral_mono restricted to set

Stream: Is there code for X?

[Alex Kontorovich]

We have MeasureTheory.set_integral_mono, but it asks for f ≤ g everywhere; we should only need this restricted to s, right? That is, does this really not exist?

theorem MeasureTheory.set_integral_mono' {X : Type*} [MeasurableSpace X]
    {μ : MeasureTheory.Measure X} {f : X → ℝ} {g : X → ℝ} {s : Set X}
    (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ)
    (h : ∀ x ∈ s, f x ≤ g x) :
    ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ := by
  sorry

[Josha Dekker]

I think the other is easier in some (but certainly not all!) situations, but this one would certainly be good to have!

[Ruben Van de Velde]

That's docs#MeasureTheory.set_integral_mono_on_ae if s is measurable

[Alex Kontorovich]

Great thanks! That's what I was looking for...

[Alex Kontorovich]

Ok docs#MeasureTheory.set_integral_mono_on is exactly what I wanted...