Zulip Chat Archive

Stream: maths

Topic: Interval integral module docstring


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 23 2020 at 21:01):

Maybe that paragraph could contain a very quick warning then.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Sep 23 2020 at 21:02):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 24 2020 at 20:31):

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

view this post on Zulip Yury G. Kudryashov (Sep 24 2020 at 21:10):

docs#interval_integrable

view this post on Zulip Yury G. Kudryashov (Sep 24 2020 at 21:11):

(deleted)


Last updated: May 09 2021 at 09:11 UTC