Zulip Chat Archive

Stream: maths

Topic: Borel measure space


view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 22:50):

It seems that the current setup (measure_space extends measurable_space, borel is an instance turning topological_space into measurable_space) it's hard to say "assume that α is a space with topology and measure, and every open set is measurable".

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 22:51):

I mean, [measure_space α] [topological_space α] creates two instances of [measurable_space α].

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 22:52):

Probably we should have [borel_measurable α] defined similarly to [order_topology α] but assuming inequality instead of equality.

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 23:34):

Another issue: for f : real → real, continuous f → measurable f is true if we take Borel sigma-algebra but fails if we add all sets of Lebesgue measure zero.

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 23:35):

So, which sigma-algebra should be the default one? And how should we handle situations when one wants to deal with Borel in the codomain and Lebesgue in the domain?

view this post on Zulip Yury G. Kudryashov (Mar 31 2020 at 23:42):

Of course, we can have a type tag for one of the spaces but this way we'll need to define a lot of instances for the "other" type, and we'll have similar issues with other topological spaces.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 03:12):

It seems that now we use Lebesgue measure but Borel σ-algebra.

view this post on Zulip Sebastien Gouezel (Apr 01 2020 at 08:03):

I think in 99% of applications people will want measurable maps to mean measurable maps with respect to the Borel sigma algebra, so this should be the default setup. But we should be able to override this. A typeclass opens_measurable α on top of [measure_space α] [topological_space α] as you suggest seems like a good setup. We should also make sure that the measurable_space structure coming from a measure space should have higher prority than the measurable_space structure coming from the topology. Or we could declare the measurable_space structure coming from the topology just as a def, and let the user declare it as an instance when needed (or put it in a locale). What are your thoughts?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:10):

I'm rewriting with def borel := ..., class borel_space [topological_space α] [measurable_space α] := (measurable_eq : ... = borel α)

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:13):

Now I'm not sure if we need class opens_measurable because it might be a good idea to use some specific predicate like lebesgue.is_measurable (don't remember exact name) in case a user wants to deal with non-Borel is_measurable on a topological space.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:23):

I'm surprised you say 99% borel, since my impression is that in analysis the lebesgue measure is the only one that matters

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:24):

I think @Sebastien Gouezel says that 99% of functions are actually (Borel, Borel) measurable.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:25):

So that you can actually work with the restriction of Lebesgue measure to the Borel σ-algebra.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:25):

I will grant that Borel has nicer closure properties

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:27):

Disclaimer: I usually want to iterate maps, so i want the same σ-algebra both in domain and codomain; then Borel is the only choice that guarantees continuous f → measurable f.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:29):

From a proof engineering perspective, it would be better to have Borel as the default, because the instance that supplies it works on any topological space, while the one for the lebesgue measure only works on real and isn't defeq

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:31):

It seems that we'll have to turn it into a class borel_space [topological_space α] [measurable_space α] := ...

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:32):

I don't follow. Why such a convoluted setup?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:32):

Because otherwise I see no way to say "I have topological_space α, measure_space α, and they agree on measurable_space α" in a theorem.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:33):

It's similar to order_closed_topology / order_topology.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:33):

If you have a topological space, and the measure space structure is the borel space, then you have that

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:33):

What should I write in example {α : Type*} [topological_space α] [measure_space α] ... : ...?

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:34):

It would just be example {α : Type*} [topological_space α] ... : ...

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:34):

Note measure_space, not measurable_space

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:34):

It would be example {α : Type*} [topological_space α] [@measure_space α (borel_measure α _inst_1)] ... : ...

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:35):

(you don't have to write that, it's the default instance)

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:35):

Also in this case we measure_space extends measurable_space

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:35):

Also we won't have to deal with two different measurable_space structures on prod.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:36):

I see, so how about class borel_measure_space A extends topological_space A, measure_space A := ...

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:45):

No, we already have a hierarchy over topological spaces. I don't want to introduce normed measure fields

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:46):

We already use this approach for algebra vs topology and order vs topology, why not use it here?

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:48):

where is the borel measurable space on an arbitrary topological space going to go?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:48):

Def

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:49):

Like preorder.topology

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:49):

so then how is this going to work with an actual borel_space?

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:50):

what data is even in the borel_space structure?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:51):

Equality between measurable_space instance and borel

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:51):

As with order_topology

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:52):

is there any example of a measure space that is eq but not defeq to borel?

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:53):

the reason this exists for order_topology is because such examples are common, e.g. the reals

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:53):

Product of two reals?

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 08:54):

Yury G. Kudryashov said:

Product of two reals?

This reminds me of the metric space / topological space thing, where we have the topology inbuilt into the definition of a metric space.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:55):

I mean, real × real with measurable_space coming from prod.measurable_space, not borel.

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:55):

right, that's what kevin means

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:56):

I think the difference in this case is that we actually have different measurable spaces floating around, and don't necessarily want to declare that every topological space can only have the canonical measurable space on it (borel)

view this post on Zulip Mario Carneiro (Apr 01 2020 at 08:56):

whereas if we have a metric space it is reasonable to ask that it never have a topological structure other than the induced one

view this post on Zulip Sebastien Gouezel (Apr 01 2020 at 08:58):

Yes, for instance on the real line you have two different natural measurable space structures, the Borel one, and the one where you declare that all sets with zero Lebesgue measure are also measurable.


Last updated: May 18 2021 at 07:19 UTC