## Stream: maths

### Topic: integral refactor

#### Yury G. Kudryashov (Jun 14 2020 at 18:03):

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 (Jun 14 2020 at 18:13):

I agree with all of this.

#### Yury G. Kudryashov (Jun 14 2020 at 18:22):

#3075 is the first step.

#### Sebastien Gouezel (Jun 14 2020 at 19:11):

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 (Jun 14 2020 at 19:25):

OK, I'll try this.

#### Jeremy Avigad (Jun 15 2020 at 15:22):

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 (Jun 15 2020 at 23:30):

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.

See #3084

#### Yury G. Kudryashov (Jun 16 2020 at 00:21):

It includes a notation #mwe

#### Yury G. Kudryashov (Jun 16 2020 at 00:21):

(tested with #3075)

#### Sebastien Gouezel (Jun 16 2020 at 07:20):

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 (Jun 16 2020 at 07:28):

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 (Jun 16 2020 at 07:30):

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 (Jun 16 2020 at 07:43):

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

#### Gabriel Ebner (Jun 16 2020 at 07:44):

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

#### Sebastien Gouezel (Jun 16 2020 at 07:45):

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 (Jun 16 2020 at 07:46):

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 (Jun 17 2020 at 14:55):

@Gabriel Ebner :up:

#### Yury G. Kudryashov (Jun 17 2020 at 14:56):

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

#### Gabriel Ebner (Jun 17 2020 at 15:03):

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 (Jun 17 2020 at 15:04):

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

#### Yury G. Kudryashov (Jun 17 2020 at 15:25):

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

#### Yury G. Kudryashov (Jun 17 2020 at 17:38):

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.