Zulip Chat Archive

Stream: maths

Topic: Lebesgue measure


view this post on Zulip Reid Barton (Sep 08 2019 at 17:28):

Do we have n-dimensional Lebesgue measure yet?

view this post on Zulip Koundinya Vajjha (Sep 08 2019 at 19:21):

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

view this post on Zulip Koundinya Vajjha (Sep 08 2019 at 19:21):

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

view this post on Zulip Reid Barton (Sep 08 2019 at 20:04):

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

view this post on Zulip Jesse Michael Han (Sep 08 2019 at 20:37):

probably an iterated binary product instead of mathlib vectors

view this post on Zulip Koundinya Vajjha (Sep 08 2019 at 21:00):

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

view this post on Zulip Kenny Lau (Sep 09 2019 at 00:10):

how about fin n -> \R

view this post on Zulip Jeremy Avigad (Sep 09 2019 at 14:44):

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.

view this post on Zulip Mario Carneiro (Sep 09 2019 at 15:07):

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

view this post on Zulip Mario Carneiro (Sep 09 2019 at 15:08):

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

view this post on Zulip Floris van Doorn (Sep 09 2019 at 15:20):

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.


Last updated: May 10 2021 at 07:15 UTC