Zulip Chat Archive

Stream: maths

Topic: Fintype as measurable spaces?


view this post on Zulip Frédéric Dupuis (Jul 22 2020 at 03:53):

Is there a reason why fintypes are not automatically declared as measurables spaces? I.e. would adding something like

instance fintype.is_measurable_space {β : Type*} [fintype β] : measurable_space β := 

to measure_theory/measurable_space.lean make sense or is there a subtle issue I'm missing?

view this post on Zulip Scott Morrison (Jul 22 2020 at 05:29):

We try to be cautious about adding unconstrained typeclasses, because they add a lot of work in the typeclass search. (Instances which only fire when certain structure appears are fine.)

view this post on Zulip Scott Morrison (Jul 22 2020 at 05:29):

I'm not sure if that was a consideration here.

view this post on Zulip Scott Morrison (Jul 22 2020 at 05:29):

It's also possible that no one has wanted this instance enough yet.

view this post on Zulip Johan Commelin (Jul 22 2020 at 05:40):

What does \top mean here? This should be simply the counting measure, right?

view this post on Zulip Johan Commelin (Jul 22 2020 at 05:41):

But what if I want to count the elements of my fintype with different weights?

view this post on Zulip Johan Commelin (Jul 22 2020 at 05:42):

Maybe the library actually supports that nowadays. Having one measure inferred by typeclass inference, but also have others around explicitly.

view this post on Zulip Yury G. Kudryashov (Jul 22 2020 at 05:59):

measurable_space is about a fixed sigma-algebra, not a measure.

view this post on Zulip Yury G. Kudryashov (Jul 22 2020 at 05:59):

Currently integrals take measure argument.

view this post on Zulip Yury G. Kudryashov (Jul 22 2020 at 05:59):

So you can have, e.g., counting.with_density f.

view this post on Zulip Yury G. Kudryashov (Jul 22 2020 at 06:01):

I mean ∫ x, f x ∂(count.with_density g)

view this post on Zulip Yury G. Kudryashov (Jul 22 2020 at 06:01):

And \top for measurable_space means "every set is measurable", like \bot for topological_space.

view this post on Zulip Johan Commelin (Jul 22 2020 at 06:04):

Aaah right. I was being confused. So that instance definitely makes sense

view this post on Zulip Frédéric Dupuis (Jul 22 2020 at 14:28):

Yes, basically this would go alongside these:

instance : measurable_space empty := 
instance : measurable_space unit := 
instance : measurable_space bool := 
instance : measurable_space  := 
instance : measurable_space  := 
instance : measurable_space  := 

I was interested in this because I was thinking of doing some probability theory, and in the discrete case it would be really inconvenient to have to explicitly specify that things are measurable all the time.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 04:03):

I think that we should have a typeclass for "all sets are measurable".

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 04:03):

Like src#discrete_topology

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 04:04):

Note that some facts from probability theory work for any measure with μ univ = 1.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 04:05):

Please don't assume [fintype] everywhere.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 04:08):

I think that we should have at least the following typeclasses (possibly under different names):

  1. probability_measure (μ : measure α) := (meas_univ_1 : μ univ = 1);
  2. finite_measure (μ : measure α) := (meas_univ_fin : μ univ < \top);
  3. no_atoms_measure (μ : measure α) := (meas_singleton : ∀ x, μ {x} = 0);

@Sebastien Gouezel what else comes to your mind?

view this post on Zulip Frédéric Dupuis (Jul 23 2020 at 21:32):

Yes, assuming [fintype] everywhere is precisely what I wanted to avoid: I want to work on the general case while making sure that the results can then be used comfortably in the discrete case. Those typeclasses sound good.


Last updated: May 14 2021 at 18:28 UTC