[Merged by Bors] - feat(measure_theory/interval_integral): weaken assumption in integral_non_ae_measurable

[benjamindavidson]

I don't see any reason for having a strict inequality here.

[benjamindavidson]

On second thought, should I just add

lemma integral_non_ae_measurable {f : α → E} {a b}
  (hf : ¬ ae_measurable f (μ.restrict (Ioc (min a b) (max a b)))) :
  ∫ x in a..b, f x ∂μ = 0 :=
by cases le_total a b; simpa [integral_of_le, integral_of_ge, h] using integral_non_ae_measurable hf

from which I can then derive an of_le version?

[urkud]

On second thought, should I just add

lemma integral_non_ae_measurable {f : α → E} {a b}
  (hf : ¬ ae_measurable f (μ.restrict (Ioc (min a b) (max a b)))) :
  ∫ x in a..b, f x ∂μ = 0 :=
by cases le_total a b; simpa [integral_of_le, integral_of_ge, h] using integral_non_ae_measurable hf

from which I can then derive an of_le version?

Do we ever need this more general lemma? Anyway,
bors d+

[bors]

✌️ benjamindavidson can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[benjamindavidson]

On second thought, should I just add

lemma integral_non_ae_measurable {f : α → E} {a b}
  (hf : ¬ ae_measurable f (μ.restrict (Ioc (min a b) (max a b)))) :
  ∫ x in a..b, f x ∂μ = 0 :=
by cases le_total a b; simpa [integral_of_le, integral_of_ge, h] using integral_non_ae_measurable hf

from which I can then derive an of_le version?

Do we ever need this more general lemma? Anyway,
bors d+

I'm not sure, but in theory it would be more suitable for the interval_integral lemmas I've been working with which don't make any assumptions about a and b. In this case it anyway feels more proper to me to show the general case and then derive the more practical case from it.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests