## Stream: maths

### Topic: product measures

#### Floris van Doorn (Aug 07 2020 at 17:53):

I'm working on product measures in a new branch, with the goal to get Fubini's theorem (which is used in all proofs that I saw that prove uniqueness of the Haar measure):
https://github.com/leanprover-community/mathlib/compare/measure-prod

Before I go to far, I want to get some discussion going on the setup I'm using, so that the library is usable.
When we talk about products, there are different things I can mean:
(1) binary products α × β;
(2) finitary products Π (i : ι), α i with [fintype ι];
(3) countable products Π (i : ι), α i with [encodable ι];
(4) arbitrary products Π (i : ι), α i.

We definitely want (1) and (2). Usually in books (2) is given as "iterate (1), and we either explicitly or implicitly all the ways that this is not convenient".
I'm currently doing (2) directly. I'm wondering how easy it is to get (1) as special case of (2). I'm a little worried about universe levels , so I'm wondering whether it is just easier to do all proofs for (1) separately. (I could try to transport along measurable_equiv (α × β) (Π (i : bool), cond (ulift α) (ulift β)), but that doesn't sound very convenient.)

How important is (3) in applications? Should I make (3) the basic definition, and (2) a special case of it? I don't think we have a multiplicative version of docs#tsum yet, right?

Most books assume σ-finiteness of measures the moment they talk about product measures. Currently I'm defining the product measure without this condition (in this case, I believe that the product measure is not unique, but I'm defining the maximal one), and I'm only going to assume it once I need it (and according to Wikipedia, Fubini's theorem even holds without σ-finiteness for the maximal product measure).

Lastly, the product measure of a complete measure is not itself complete. So the product measure on ℝ × ℝ is not the same as the Lebesque measure. My intuition is that this doesn't really matter for us, since every measure comes with its own outer measure anyway.

Any thoughts or comments are welcome!
@Yury G. Kudryashov @Joe @Johannes Hölzl

#### Yury G. Kudryashov (Aug 07 2020 at 19:55):

If we want to have a sequence of identically distributed random variables some day, then probably we need the product measure on nat → α.

#### Yury G. Kudryashov (Aug 07 2020 at 19:56):

I have no opinion about $\sigma$-finiteness.

#### Sebastien Gouezel (Aug 07 2020 at 20:01):

Except that it's not the product measure in the usual sense when the product is infinite, you need some extension theorem (like Kolmogorov or Ionescu-Tulcea) to define the infinite product measure, and it only makes sense for probability measures. So I would say this is different enough that you can concentrate on finite products for now, and we will come back to the infinite product when needed.

#### Sebastien Gouezel (Aug 07 2020 at 20:27):

Floris van Doorn said:

Lastly, the product measure of a complete measure is not itself complete. So the product measure on ℝ × ℝ is not the same as the Lebesque measure. My intuition is that this doesn't really matter for us, since every measure comes with its own outer measure anyway.

I am not sure I get this. If you take the product measure of Lebesgue measure with the Borel sigma-algebra, you again get Lebesgue measure with the Borel sigma-algebra, right? The problem only appears when you consider completed sigma-algebras, but this is less usual than the Borel one.

#### Yury G. Kudryashov (Aug 07 2020 at 20:47):

Anyway I think that we should have Borel as the main sigma-algebra and use predicates for "measurable w.r.t. the completed sigma-algebra".

#### Floris van Doorn (Aug 07 2020 at 21:04):

Yes, the (finitary) product of borel sigma-algebras is again borel: docs#prod.borel_space . If the Borel sigma-algebra is the main one we use, then there is no problem.

#### Yury G. Kudryashov (Aug 07 2020 at 21:31):

Once someone will want to integrate functions measurable w.r.t. (Lebesgue, Borel), we'll need to migrate the integration to is_null_measurable.

#### Yury G. Kudryashov (Aug 07 2020 at 21:32):

BTW, it's hard to tell from names that is_measurable is about sets and measurable is about functions. What about measurable_set and measurable_fun?

#### Yury G. Kudryashov (Aug 07 2020 at 21:34):

Another question: what are you plans about real.measure_space? Should we redefine it as haar_measure (Icc 0 1) 1?

#### Floris van Doorn (Aug 07 2020 at 21:58):

Yury G. Kudryashov said:

BTW, it's hard to tell from names that is_measurable is about sets and measurable is about functions. What about measurable_set and measurable_fun?

Yeah, I have noticed the same. I don't mind it, but changing it is probably good.

Yury G. Kudryashov said:

Another question: what are you plans about real.measure_space? Should we redefine it as haar_measure (Icc 0 1) 1?

Yes, I think that would be good.

#### Floris van Doorn (Aug 07 2020 at 21:59):

That might require us to @[to_additive] everything in my recent PRs.

#### Mario Carneiro (Aug 07 2020 at 22:31):

Could we get dot notation working? @Gabriel Ebner can we get dot notation to work on pi types as if they were in the Pi namespace?

#### Yury G. Kudryashov (Aug 07 2020 at 22:36):

Last time this question was asked Gabriel pointed to the function in C++ source that has to be modified.

#### Yury G. Kudryashov (Aug 07 2020 at 22:37):

Note that users might want pi, forall, or function depending on the actual type.

#### Mario Carneiro (Aug 07 2020 at 22:39):

I think for the sake of determinism we should just always use Pi

#### Floris van Doorn (Aug 08 2020 at 07:14):

Interesting: I was thinking of a different potential feature of the dot notation for functions, namely if e : Π x1 x2 x3, foo t1 t2 t3 then e.bar means foo.bar e.
This allows you to write

• if m : Π i, outer_measure (α i) then m.pi is outer_measure.pi m
• if μ : Π i, measure (α i) then μ.pi is measure.pi μ
etc.

#### Yury G. Kudryashov (Aug 09 2020 at 01:54):

BTW, did you see #2819?

#### Yury G. Kudryashov (Aug 09 2020 at 02:21):

BTW, they use bundled probability measures with coe_fn sending sets to nnreals. @Sebastien Gouezel @Floris van Doorn Do you have an opinion on whether we want this or you prefer to have a typeclass?

#### Yury G. Kudryashov (Aug 09 2020 at 02:29):

(of course, integration should use coercion to measure)

#### Floris van Doorn (Aug 09 2020 at 04:13):

Ah, thanks for pointing me to that. I know about the project, but I forgot that they also did product measures there.
Can you define finitary product measures using the Giry monad (without doing recursion) ?
So far I'm only working on finitary product measures, so there doesn't seem to be much overlap yet, but it's good to remember that product measure has already been done.
(let me also ping @Alex J. Best @Koundinya Vajjha to this topic)

#### Floris van Doorn (Aug 09 2020 at 04:13):

I don't have a strong opinion whether measures should be typeclasses or bundled.
I like the use of bundled measures so far, and have not yet used measure_space/volume.

#### Yury G. Kudryashov (Aug 13 2020 at 03:34):

My question was not about volume vs μ : measure α (I did the refactor moving from volume to μ in integrals). My question is whether we want (μ : probability_measure α) or (μ : measure α) [probability_measure μ].

#### Yury G. Kudryashov (Aug 13 2020 at 03:36):

BTW, I have a proof of the following fact: if two locally finite measures on real are equal on all intervals with rational endpoints, then they're equal + corollaries about measure.map f volume with f = ((+) a), f = ((*) a), f = has_neg.neg. It's not ready for review yet.

#### Yury G. Kudryashov (Aug 13 2020 at 03:36):

(of course, the proof starts with a more general fact)

#### Yury G. Kudryashov (Aug 13 2020 at 04:08):

The proof is in this branch

#### Floris van Doorn (Aug 21 2020 at 18:55):

Is the following statement true in general? I want it to use it for the product measure. But for example in #2819 it is only proven specifically for the case where f = prod.mk.

import measure_theory.giry_monad
open measure_theory measure_theory.measure

lemma measurable.map {α β ι} [measurable_space ι] [measurable_space α] [measurable_space β]
{f : ι → α → β} {μ : measure α} (hf : ∀ i, measurable (f i))
(hf2 : measurable f) : measurable (λx, map (f x) μ) := sorry


#### Adam Topaz (Aug 21 2020 at 19:03):

I think this might be relevant: https://ncatlab.org/nlab/show/strong+monad see the last example in section 4.

#### Floris van Doorn (Aug 21 2020 at 19:15):

That does look relevant indeed. I don't quite understand its implications.

#### Adam Topaz (Aug 21 2020 at 19:16):

I think the main thing is that the giry monad should be "commutative" (with respect to the cartesian monoidal structure).

#### Adam Topaz (Aug 21 2020 at 19:19):

Oh, but this looks to fail with this other monoidal structure defined in this paper: https://arxiv.org/pdf/1612.05939.pdf

#### Adam Topaz (Aug 21 2020 at 19:20):

@Bhavik Mehta told me about commutative monads a little while ago, maybe he has some ideas.

#### Floris van Doorn (Aug 21 2020 at 19:35):

The commutativity exactly corresponds to the fact that the product of measures is "commutative" in the appropriate way. I have proven that modulo the above fact.

Oh I see.

#### Adam Topaz (Aug 21 2020 at 19:50):

Wait, now I'm confused. What does measurable f mean? Isn't this saying that the function from \iotato \a \to \b is measurable, which implicitly assumes that \a \to \b is measurable?

#### Floris van Doorn (Aug 21 2020 at 19:51):

yes, it is a measurable map into a function space. It is equivalent to the first component being measurable:

lemma measurable_pi {f : γ → Πa, β a} : measurable f ↔ ∀ x, measurable (λ c, f c x)


#### Floris van Doorn (Aug 21 2020 at 19:52):

(I proved that on a branch, but it's just combining measurable_pi_apply and measurable_pi_lambda)

#### Adam Topaz (Aug 21 2020 at 19:53):

But wouldn't this imply that that you're working in a cartesian closed category? Or is this not actually the internal hom in the category of measurable spaces.

#### Adam Topaz (Aug 21 2020 at 19:54):

I guess I'm trying to understand whether the negative result in that arxiv link actually applies.

#### Floris van Doorn (Aug 21 2020 at 20:03):

α → β is not the internal hom in the category of measurable spaces, it's an infinite product of measurable spaces.
I don't think that the arxiv link is relevant: it's about a different monoidal structure, which I don't think I use.

#### Adam Topaz (Aug 21 2020 at 20:16):

So what's stopping the function $x \mapsto (\lambda c, f( c,x))$ from being completely crazy?

#### Floris van Doorn (Aug 21 2020 at 20:18):

You mean in the original question? I added the condition measurable f, which is equivalent to ∀ x, measurable (λ c, f c x).

#### Adam Topaz (Aug 21 2020 at 20:20):

The function $\alpha \to (\iota \to \beta)$ given by $x \mapsto (i \mapsto f(i,x))$ need not be measurable, right?

#### Adam Topaz (Aug 21 2020 at 20:21):

Yes, I'm talking about the original question of whether the lemma is correct.

#### Adam Topaz (Aug 21 2020 at 20:21):

Oh never mind. Missed that additional assumption hf.

#### Adam Topaz (Aug 21 2020 at 20:24):

I guess hfis saying swap f is measurable, right?

correct

#### Floris van Doorn (Aug 26 2020 at 20:58):

Update:
In the branch https://github.com/leanprover-community/mathlib/compare/measure-prod I defined binary product measures (for sigma-finite measures), and proved Tonelli's Theorem. Fubini's Theorem is next.

@Yury G. Kudryashov Do you have a chance to look at #3760 soon? (Or otherwise do you mind if I incorporate my suggestions and merge it?)

#### Floris van Doorn (Aug 27 2020 at 19:48):

@Yury G. Kudryashov I'm now working with the integrable predicate, and I'm sad that integrable does not include measurable. Almost always when you require integrability you also require measurability.
How do you feel about changing integrable f μ so that it includes measurable f?

I agree.

#### Floris van Doorn (Sep 16 2020 at 01:27):

@Yury G. Kudryashov @Patrick Massot I started working on adding measurability to the integrable predicate. It simplifies a lot of things. The only drawback I noticed is that I had to add a borel_spaceinstance in a few places.

#### Floris van Doorn (Sep 16 2020 at 01:27):

https://github.com/leanprover-community/mathlib/compare/integrable

#### Yury G. Kudryashov (Sep 16 2020 at 04:19):

I need a couple of days without other measure_theory refactors going on to rename measurablemeasurable_fun, is_measurablemeasurable_set. This is a low priority change but I don't want to avoid merge conflicts. Please ping me once your current refactors (including "integrable implies measurable") will be merged.

#### Floris van Doorn (Sep 16 2020 at 04:20):

ok, I'll finish this refactor in the next few days.

#### Yury G. Kudryashov (Sep 16 2020 at 04:24):

For now I'm rewriting simple_func_dense: I want a simpler proof and a version that ensures F n x ∈ range f.

#### Patrick Massot (Sep 16 2020 at 07:38):

I like this change but, as discussed here, I also have integration PRs in the pipeline.

#### Yury G. Kudryashov (Sep 16 2020 at 18:37):

AFAIR, your PRs are localized additions, not refactoring. I'm ready to resolve merge conflicts in this case. I want to avoid merging to refactoring commits.

#### Floris van Doorn (Sep 25 2020 at 22:30):

I proved Fubini's theorem in https://github.com/leanprover-community/mathlib/compare/measure-prod
These PR's have some preliminary stuff: #4262 #4263 #4264 #4265 #4266
I plan to open 1 more PR with general measure theory (100-200 lines) and then 1 PR which just adds the file measure_theory.prod containing Tonelli's theorem and Fubini's theorem (600-800 lines)

Last updated: May 10 2021 at 08:14 UTC