integral refactor

Stream: maths

[Yury G. Kudryashov]

Hello, I propose the following refactor of integrals; the design is partially based on big_operators.

1. The main definition is the integral of a function w.r.t. an explicit measure μ on a set s.
2. We have special notation for the cases s = univ and μ = volume.
3. Most theorems take s and μ as implicit arguments.
4. We still need a special notation/definition for $\int_a^b f(x)\,dx$ because we want $\int_b^a f(x)\,dx=-\int_a^b f(x)\,dx$.

[Sebastien Gouezel]

I agree with all of this.

[Yury G. Kudryashov]

#3075 is the first step.

[Sebastien Gouezel]

I am not sure it is worth going through small steps in such a big refactor: it will be painful to have something coherent at every step, and these PRs will also be hard to review if we don't know the bigger picture. Maybe you can just tell us here on Zulip what the main definitions and notations would be, then we discuss it here, and once we're all happy you can go for a giant PR that I will try to review quickly.

[Yury G. Kudryashov]

OK, I'll try this.

[Jeremy Avigad]

This sounds good to me. In Isabelle it was always painful having so many variations on the integral. I think this is the most elegant way to simplify and standardize.

[Yury G. Kudryashov]

I am not sure it is worth going through small steps in such a big refactor

Now I'm not sure that this is true. One of my goals is to make the new code "almost" backwards compatible with the old code. More precisely, old code using notation (and not functions) should compile, possibly after some search&replace of lemma names. Another reason to go with smaller PRs is that I'm very bad at refactoring one part of a library without touching other parts.

and these PRs will also be hard to review if we don't know the bigger picture

Sure. I'll try to describe my plan tonight.

[Yury G. Kudryashov]

See #3084

[Yury G. Kudryashov]

It includes a notation #mwe

[Yury G. Kudryashov]

(tested with #3075)

[Sebastien Gouezel]

This looks great to me, except that I would put ∂ μ at the end, if this is possible with Lean's notation system (I mean, write ∫⁻ x in t, 1 ∂ volume. Also, do you have plans for more restricted classes of measures, say probability measures (or sigma-finite measures, or whatever)? It is easy to provide a typeclass extending measure_space specifying that volume should have mass 1, and to state theorems under this typeclass assumption, but it wouldn't make them easily available for any probability measure on any measure space without the typeclass. And conversely I don't see an easy mechanism to state the theorem in general with an assumption that would be filled automatically when dealing with a probability coming from the typeclass -- a default tactic for the assumption, maybe?

[Yury G. Kudryashov]

About notation: I copied notation for sums and slightly modified it. I don't know the full syntax of Lean notation command. I hope that someone with more experience with notation can help.

@Mario Carneiro @Gabriel Ebner :up: (who else should I tag on questions like this one?)

[Yury G. Kudryashov]

We can have @[class] def probability_measure (μ : measure α) := μ univ = 1, a class probability_space, and an instance [probability_space α] : probability_measure (volume : measure α).

[Gabriel Ebner]

The notations look fine. We should probably adjust the precedence a little bit so that ∫⁻ x, 0 = 0 parses as expected.

[Gabriel Ebner]

That is, probably notation `∫⁻` binders `, ` r:(scoped:67 f, lintegral volume set.univ f) := r

[Sebastien Gouezel]

Yury G. Kudryashov said:

We can have @[class] def probability_measure (μ : measure α) := μ univ = 1, a class probability_space, and an instance [probability_space α] : probability_measure (volume : measure α).

Yes, looks perfect!

[Sebastien Gouezel]

Gabriel Ebner said:

The notations look fine.

I was asking if it is possible to put the measure at the end, to write ∫⁻ x in t, 1 ∂ volume. Then the notation incantation should be different, and Yury doesn't know how to do it.

[Yury G. Kudryashov]

@Gabriel Ebner :up:

[Yury G. Kudryashov]

Is it easy/possible with notation? Of course, we can reorder arguments in the definition if it would help.

[Gabriel Ebner]

import measure_theory.measure_space

variables {α : Type*} {β : Type*} [measurable_space α]
noncomputable theory

namespace measure_theory

variables [measure_space β] (s : set α) (t : set β)

def lintegral (μ : measure α) (s : set α) (f : α → ennreal) : ennreal := 0

notation `∫⁻` binders ` in ` s `, ` r:(scoped:67 f, f) ` ∂ ` μ := lintegral μ s r
notation `∫⁻` binders ` in ` s `, ` r:(scoped:67 f, lintegral volume s f) := r
notation `∫⁻` binders `, ` r:(scoped:67 f, f) ` ∂ ` μ := lintegral μ set.univ r
notation `∫⁻` binders `, ` r:(scoped:67 f, lintegral volume set.univ f) := r

variables (μ : measure α)

#check ∫⁻ (x : β), 0
#check ∫⁻ (x : β), 0 ∂ volume
#check ∫⁻ (x : α), 0 ∂ μ
#check ∫⁻ x, 0 ∂ μ
#check ∫⁻ x in t, 1
#check ∫⁻ x in s, 2 ∂ μ
#check ∫⁻ x in t, 1 ∂ volume
#check ∫⁻ (x : β) in set.univ, 1 ∂ volume

end measure_theory

[Gabriel Ebner]

It's not perfect, for example ∫⁻ x y, 0 ∂ μ doesn't work.

[Yury G. Kudryashov]

Thanks a lot! I think that we can live with ∫⁻ (x : α), (∫⁻ (y : β), 0) ∂ μ for double integrals.

[Yury G. Kudryashov]

@Sebastien Gouezel ping about #3075

[Yury G. Kudryashov]

The first draft of measure_theory/integration is in #3373. I decided to exclude s from the definition and use notation to enter ∫⁻ x, f x ∂(restrict s μ) as ∫⁻ x in s, f x ∂ μ (and not ∫⁻ x, indicator s f x ∂ μ). The main reason is that theorems that do not care about s can be formulated without it and be useful for ∫⁻ x in s, f x ∂μ.

@Sebastien Gouezel Could you please have a look at integration.lean? If you're happy with these changes, I'll adjust the rest of measure_theory/ to the new API and rewrite bochner_integration using the same style. Note: for most lemmas/theorems I just changed the notation. In particular, I rarely tried to rewrite (or even carefully read) a proof.

@Gabriel Ebner Could you please have a look at notations here? While Lean accepts ∫⁻ x in s, f x ∂μ, it prints ∫⁻ x, f x ∂(restrict s μ) in the proof state.