Interval integral module docstring

Stream: maths

[Patrick Massot]

@Yury G. Kudryashov did you really meant to write https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/interval_integral.lean#L13-L14? It seems inconsistent with the actual definition.

[Yury G. Kudryashov]

This paragraph describes something that can't be a definition in lean: a=b matches both ifs. AFAIR, or guidelines allow mathematically but not formally true descriptions in the docstrings. The actual definition is discussed in the section "implementation details". If you prefer to have a formally correct explanation right away, then feel free to reformulate the docstrings.

[Patrick Massot]

Maybe that paragraph could contain a very quick warning then.

[Patrick Massot]

Since you're here, is there any kind of general procedure to deduce stuff for interval_integral from the corresponding stuff for the general theory?

[Patrick Massot]

(I mean in Lean of course, in maths there is no problem)

[Yury G. Kudryashov]

There are two ways: (1) unfold the definition and rewrite each integral; (2) by_cases h : le_total a b (or some wlog), then simp to a set integral.

[Yury G. Kudryashov]

Note that ∫ x in Ioc a b, f x ∂μ is actually ∫ x, f x ∂(μ.restrict (Ioc a b)), so you can apply theorems about ∫ x, f x ∂μ directly.

[Patrick Massot]

Thanks. I used the first strategy before asking, but I'll keeping the second one in mind as well.

[Patrick Massot]

Another related question: do we have an analogue of integrable_on for interval integrals?

[Yury G. Kudryashov]

docs#interval_integrable

[Yury G. Kudryashov]

(deleted)