Fintype as measurable spaces?

Stream: maths

[Frédéric Dupuis]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Currently integrals take measure argument.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Frédéric Dupuis]

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]

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

[Yury G. Kudryashov]

Like src#discrete_topology

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Please don't assume [fintype] everywhere.

[Yury G. Kudryashov]

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]

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.