## Stream: maths

### Topic: Integrals w.r.t. non-canonical measures

#### Yury G. Kudryashov (Jan 23 2020 at 04:41):

Currently the "main" integral in measure_theory is the integral (Lebesgue or Bochner) w.r.t. the canonical measure. There is a rudimentary interface for computing integrals w.r.t. non-canonical measures but it lags behind the "main" one, and one has to restate all theorems before using them.
I know quite a few theorems dealing with non-canonical measures or even with the space of measures. The simplest example is the substitution rule; actually it says something about push forward of a measure. There are many more advanced examples in dynamical systems, especially in ergodic theory.
I propose to refactor it so that all definitions/theorems take measure as an argument. It shouldn't be too hard to write variables (m : measure α) instead of [measure_space α], then prefix each apply with m.. This way it will be easy to apply these theorems both to the canonical measure and non-canonical measures. E.g., we can leave current binder notation for integrals w.r.t. the canonical measure, and add some other notation for integrals w.r.t. any measure.
Do I miss something?

#### Mario Carneiro (Jan 23 2020 at 07:27):

I would like common / important theorems to be restated with the notation, but I think it would be a good idea to do the main development in this context.

#### Sebastien Gouezel (Jan 23 2020 at 08:29):

I also think it is important to have all theorems and the main developments done with a typeclass measure. For instance, later on when you do probability theory, or ergodic theory with a fixed reference measure, you don't want to give explicitly the measure in all applications of lemmas. But I also agree that we will need versions taking the measure as an argument. Either by stating the most important lemmas in this context, or by crafting an attribute @[with_explicit_measure]...

#### Johan Commelin (Jan 23 2020 at 08:33):

I like the idea of an attribute that creates a copy of the declaration in which the measure is explicit.

#### Yury G. Kudryashov (Jan 23 2020 at 13:19):

If we have a notation μ := volume then giving this parameter explicitly takes only 2 characters (space and μ).

#### Chris Hughes (Jan 23 2020 at 13:20):

You could even do local notation for those files.

#### Yury G. Kudryashov (Jan 23 2020 at 13:21):

Yes, this could be a localized notation.

#### Yury G. Kudryashov (Jan 23 2020 at 13:21):

Then we won't need to have 2 versions of each theorem.

#### Chris Hughes (Jan 23 2020 at 13:24):

What I meant was that you could do local notation for integral μ or whatever.

#### Yury G. Kudryashov (Jan 23 2020 at 13:38):

@Chris Hughes Which setup are you talking about: (1, current) stating theorems for the canonical measure, restating some of them for any measure; or (2) stating theorems for any measure, reusing for the canonical measure?

2

#### Yury G. Kudryashov (Jan 23 2020 at 13:44):

Yes, I think that we should leave the current notation for integrals, and use a new one for integrals w.r.t. any measure.

#### Yury G. Kudryashov (Jan 23 2020 at 13:47):

@Sebastien Gouezel In many cases (simp, rw, apply) you can just name the lemma, and let Lean figure out m = volume itself. In other cases I don't think that writing  μ takes a lot of time.

#### Yury G. Kudryashov (Jan 23 2020 at 13:48):

@Mario Carneiro To be sure: which context did you mean by "this context"?

#### Johan Commelin (Jan 23 2020 at 13:55):

@Yury G. Kudryashov So you suggest to make the measure explicit everywhere?

#### Yury G. Kudryashov (Jan 23 2020 at 13:55):

@Johan Commelin Yes.

#### Yury G. Kudryashov (Jan 23 2020 at 13:56):

/me disappears for a few hours.

#### Johan Commelin (Jan 23 2020 at 13:56):

def μ := infer_instance ??

#### Yury G. Kudryashov (Jan 23 2020 at 15:05):

More like notation mu = volume

#### Joe (Jan 23 2020 at 16:12):

I tried to do this several weeks ago. Here are some difficulties. I guess one challenge is how to write binder notations like ∫ a, f a or ∀ₘ a, 0 ≤ f a. If not using the binder notation, sometimes I just feel there are too many parameters and I tend to mess up their orders.

#### Joe (Jan 23 2020 at 16:12):

A second thing is namespaces and theorem names. There are three versions of integrals : integral, integral on a subset, integral on an interval. Maybe there will be more in the future. Right now you can put the first integral (and its related theorems) in the namespace measure_theory, the second integral in the namespace set, the third integral in the namespace real, and call the corresponding theorems with the same name. I'm not sure what to do if everything has to be in the namespace measure_theory.measure.

#### Joe (Jan 23 2020 at 16:12):

A third thing is that you need to prefix everything with a measure even if you just want to use the default measure. For example, I only want to use the Lebesgue measure on the real line when proving the FTC.

#### Joe (Jan 23 2020 at 16:23):

By the way, with regard to the first point, I noticed that I defined measurable_on and integrable_on with variables in the order integrable_on (s : set α) (f : α → β), which is the opposite of continuous_on (f : α → β) (s : set α). I should align myself with the current convention.

But are there any rules concerning the order of variables and the use of explicit and implicit variables? I often notice inconsistencies, which is sometimes annoying, because I have to guess how many underscores I should put down.

#### Joe (Jan 23 2020 at 17:11):

So I'm thinking why not just keep two copies?

#### Yury G. Kudryashov (Jan 23 2020 at 20:04):

Thank you @Joe for detailed arguments. Now I have to go pick up kids but I'll try to read it carefully tonight or tomorrow.

Last updated: May 10 2021 at 07:15 UTC