Integrals w.r.t. non-canonical measures

Stream: maths

[Yury G. Kudryashov]

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]

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]

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]

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

[Yury G. Kudryashov]

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

[Chris Hughes]

You could even do local notation for those files.

[Yury G. Kudryashov]

Yes, this could be a localized notation.

[Yury G. Kudryashov]

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

[Chris Hughes]

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

[Yury G. Kudryashov]

@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?

[Chris Hughes]

2

[Yury G. Kudryashov]

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]

@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]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

@Johan Commelin Yes.

[Yury G. Kudryashov]

/me disappears for a few hours.

[Johan Commelin]

def μ := infer_instance ??

[Yury G. Kudryashov]

More like notation mu = volume

[Joe]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

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.