Lebesgue measure

Stream: maths

[Reid Barton]

Do we have n-dimensional Lebesgue measure yet?

[Koundinya Vajjha]

You can define it using the giry monad.
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Giry.20monad.20for.20product.20measures

[Koundinya Vajjha]

I have some stuff on this but it's in a closed repo -- will push this back to mathlib at somepoint

[Reid Barton]

How do you define $\mathbb{R}^n$?

[Jesse Michael Han]

probably an iterated binary product instead of mathlib vectors

[Koundinya Vajjha]

Yeah I found working with subtypes very painful so I switched over to iterated binary products.

[Kenny Lau]

how about fin n -> \R

[Jeremy Avigad]

For something I was doing recently, I found it useful to give that a name, tuple \R n. It doesn't save that many keystrokes, but you get to use the projection notation, which is nice.

[Mario Carneiro]

That is perhaps a better name than vector2 that is the current name in some local file or other

[Mario Carneiro]

@Floris van Doorn was arguing for using this type for vectors, I forget if dvector means this or the inductive type in flypitch

[Floris van Doorn]

In flypitch we define dvector to be the inductive family of vectors. That was before I realized how nice fin n -> \a is. I think everything we do with dvector in flypitch can be done nicer or equally nice with fin n -> \a.