Zulip Chat Archive

Stream: maths

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


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

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

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

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

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

view this post on Zulip Chris Hughes (Jan 23 2020 at 13:20):

You could even do local notation for those files.

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 13:21):

Yes, this could be a localized notation.

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 13:21):

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

view this post on Zulip Chris Hughes (Jan 23 2020 at 13:24):

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

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

view this post on Zulip Chris Hughes (Jan 23 2020 at 13:39):

2

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

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

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 13:48):

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

view this post on Zulip Johan Commelin (Jan 23 2020 at 13:55):

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

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 13:55):

@Johan Commelin Yes.

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 13:56):

/me disappears for a few hours.

view this post on Zulip Johan Commelin (Jan 23 2020 at 13:56):

def μ := infer_instance ??

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 15:05):

More like notation mu = volume

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

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

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

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

view this post on Zulip Joe (Jan 23 2020 at 17:11):

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

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