product measures

Stream: maths

[Floris van Doorn]

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]

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]

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

[Sebastien Gouezel]

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]

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]

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]

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]

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]

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]

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

[Floris van Doorn]

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]

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

[Mario Carneiro]

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]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Floris van Doorn]

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]

BTW, did you see #2819?

[Yury G. Kudryashov]

And https://github.com/jtristan/stump-learnable

[Yury G. Kudryashov]

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]

(of course, integration should use coercion to measure)

[Floris van Doorn]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

The proof is in this branch

[Floris van Doorn]

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]

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

[Floris van Doorn]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Floris van Doorn]

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.

[Adam Topaz]

Oh I see.

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

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

[Floris van Doorn]

α → β 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]

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

[Floris van Doorn]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

Oh never mind. Missed that additional assumption hf.

[Adam Topaz]

I guess hfis saying swap f is measurable, right?

[Floris van Doorn]

correct

[Floris van Doorn]

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]

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

[Yury G. Kudryashov]

I agree.

[Floris van Doorn]

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

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

[Yury G. Kudryashov]

I need a couple of days without other measure_theory refactors going on to rename measurable → measurable_fun, is_measurable → measurable_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]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

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)

[Yury G. Kudryashov]

@Floris van Doorn It turns out that prod_prod works for non-measurable sets, see #10241

[Floris van Doorn]

Oh neat! I couldn't get that to work before.