## Stream: maths

### Topic: Fintype as measurable spaces?

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

#### 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.)

#### Scott Morrison (Jul 22 2020 at 05:29):

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

#### Scott Morrison (Jul 22 2020 at 05:29):

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

#### Johan Commelin (Jul 22 2020 at 05:40):

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

#### Johan Commelin (Jul 22 2020 at 05:41):

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

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

#### Yury G. Kudryashov (Jul 22 2020 at 05:59):

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

#### Yury G. Kudryashov (Jul 22 2020 at 05:59):

Currently integrals take measure argument.

#### Yury G. Kudryashov (Jul 22 2020 at 05:59):

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

#### Yury G. Kudryashov (Jul 22 2020 at 06:01):

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

#### Yury G. Kudryashov (Jul 22 2020 at 06:01):

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

#### Johan Commelin (Jul 22 2020 at 06:04):

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

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

#### Yury G. Kudryashov (Jul 23 2020 at 04:03):

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

#### Yury G. Kudryashov (Jul 23 2020 at 04:04):

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

#### Yury G. Kudryashov (Jul 23 2020 at 04:05):

Please don't assume [fintype] everywhere.

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

#### 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