Zulip Chat Archive

Stream: maths

Topic: Borel measure space

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".

Yury G. Kudryashov (Mar 31 2020 at 22:51):

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

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.

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.

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?

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.

Yury G. Kudryashov (Apr 01 2020 at 03:12):

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

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?

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 α)

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.

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

Yury G. Kudryashov (Apr 01 2020 at 08:24):

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

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.

Mario Carneiro (Apr 01 2020 at 08:25):

I will grant that Borel has nicer closure properties

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.

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

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 α] := ...

Mario Carneiro (Apr 01 2020 at 08:32):

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

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.

Yury G. Kudryashov (Apr 01 2020 at 08:33):

It's similar to order_closed_topology / order_topology.

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

Yury G. Kudryashov (Apr 01 2020 at 08:33):

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

Mario Carneiro (Apr 01 2020 at 08:34):

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

Yury G. Kudryashov (Apr 01 2020 at 08:34):

Note measure_space, not measurable_space

Mario Carneiro (Apr 01 2020 at 08:34):

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

Mario Carneiro (Apr 01 2020 at 08:35):

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

Yury G. Kudryashov (Apr 01 2020 at 08:35):

Also in this case we measure_space extends measurable_space

Yury G. Kudryashov (Apr 01 2020 at 08:35):

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

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 := ...

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

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?

Mario Carneiro (Apr 01 2020 at 08:48):

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

Yury G. Kudryashov (Apr 01 2020 at 08:48):

Def

Yury G. Kudryashov (Apr 01 2020 at 08:49):

Like preorder.topology

Mario Carneiro (Apr 01 2020 at 08:49):

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

Mario Carneiro (Apr 01 2020 at 08:50):

what data is even in the borel_space structure?

Yury G. Kudryashov (Apr 01 2020 at 08:51):

Equality between measurable_space instance and borel

Yury G. Kudryashov (Apr 01 2020 at 08:51):

As with order_topology

Mario Carneiro (Apr 01 2020 at 08:52):

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

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

Yury G. Kudryashov (Apr 01 2020 at 08:53):

Product of two reals?

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.

Yury G. Kudryashov (Apr 01 2020 at 08:55):

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

Mario Carneiro (Apr 01 2020 at 08:55):

right, that's what kevin means

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)

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

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: Dec 20 2023 at 11:08 UTC