# Zulip Chat Archive

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

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

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