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 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 (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):

docs#interval_integrable

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

(deleted)

Last updated: May 09 2021 at 09:11 UTC