# Zulip Chat Archive

## Stream: maths

### Topic: Interval integral module docstring

#### Patrick Massot (Sep 23 2020 at 20:49):

@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 (Sep 23 2020 at 20:57):

This paragraph describes something that can't be a definition in lean: `a=b`

matches both `if`

s. 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 (Sep 23 2020 at 21:01):

Maybe that paragraph could contain a very quick warning then.

#### Patrick Massot (Sep 23 2020 at 21:02):

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 (Sep 23 2020 at 21:02):

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

#### Yury G. Kudryashov (Sep 23 2020 at 21:27):

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 (Sep 23 2020 at 21:28):

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 (Sep 24 2020 at 20:29):

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

#### Patrick Massot (Sep 24 2020 at 20:31):

Another related question: do we have an analogue of `integrable_on`

for interval integrals?

#### Yury G. Kudryashov (Sep 24 2020 at 21:10):

#### Yury G. Kudryashov (Sep 24 2020 at 21:11):

(deleted)

Last updated: May 09 2021 at 09:11 UTC