Zulip Chat Archive

Stream: new members

Topic: Probability theory


view this post on Zulip Kalle Kytölä (Apr 03 2021 at 22:45):

I definitely agree that it would be great to have much of formal ML in mathlib. It seems like a fantastic addition to probability theory and I wasn't aware of it before. Thank you Joao for pointing it out! And of course thanks to Martin Zinkevich for the whole thing!

(Btw, I think it might be best to rename this discussion's topic to something more accurately descriptive, e.g. "probability theory", maybe starting from Floris' message. Renaming topics seems to require admin rights, though.)

view this post on Zulip Bryan Gin-ge Chen (Apr 03 2021 at 23:03):

(I've renamed the thread.)

view this post on Zulip Bryan Gin-ge Chen (Apr 03 2021 at 23:07):

I think @Koundinya Vajjha's repo at https://github.com/jtristan/stump-learnable has some material on probability theory as well.

view this post on Zulip Greg Price (Apr 06 2021 at 04:42):

Heather Macbeth said:

I am not sure what the etiquette here is, not to mention the ethics and the law -- if a person writes a Lean package under an open-source license (as Martin did with FormalML), is it ok for someone else to PR parts of it, keeping the copyright and authorship intact?

As far as ethics and law is concerned, the answer is yes and this is common practice in software.

It's necessary that the licenses be compatible -- that is, the original license and that of the project the material is then contributed to must not have conditions that conflict with each other -- but it looks like Formal ML uses exactly the same license as mathlib, so that's not an issue here.

(And of course it's essential to be explicit about the original authorship, essential ethically and also legally under typical open-source licenses.)

view this post on Zulip Greg Price (Apr 06 2021 at 04:42):

That doesn't answer the question of etiquette. I think the central question there is usually how the original author is likely to feel about it.

view this post on Zulip Hunter Monroe (Apr 17 2021 at 16:19):

I just sent an email to Martin Zinkevich asking his permission to integrate FormalML into mathlib. Attached is a first attempt to integrate his file probability_space.lean into mathlib. Here is an immediate issue. He defines a probability space (see https://github.com/google/formal-ml/blob/master/src/formal_ml/probability_space.lean) as follows:

class probability_space (α: Type*) extends measure_theory.measure_space α :=
  (univ_one:volume.measure_of (set.univ) = 1)

whereas mathlib already has

class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ = 1)

How should these be reconciled? probability_space.lean Also measurable_setB needs a better name.

view this post on Zulip Mario Carneiro (Apr 17 2021 at 16:20):

Those are the same? A probability space is a measure space where the designated "volume" measure is a probability measure

view this post on Zulip Hunter Monroe (Apr 17 2021 at 16:32):

@Mario Carneiro Repeating "=1" seems redundant--one definition could rely on the other, i.e., a probability_space is a measure_space with a measure that is a probability_measure.

view this post on Zulip Mario Carneiro (Apr 17 2021 at 16:32):

That's what I just said

view this post on Zulip Mario Carneiro (Apr 17 2021 at 16:34):

I don't think it matters too much whether the field is (univ_one:volume.measure_of (set.univ) = 1) or [prob : probability_measure volume]

view this post on Zulip Mario Carneiro (Apr 17 2021 at 16:35):

the former is probably a bit more convenient when constructing probability spaces

view this post on Zulip Mario Carneiro (Apr 17 2021 at 16:35):

but you can have constructors for both versions

view this post on Zulip Eric Wieser (Apr 18 2021 at 11:19):

Judging by your first PR to attempt to integrate formalML into mathlib, it may make sense to first integrate mathlib into formalML; despite depending on mathlib, the library seems to repeat lots of our lemmas.

view this post on Zulip Eric Wieser (Apr 18 2021 at 11:20):

I guess how viable that is depends on whether Martin has the time to accept pull requests.

view this post on Zulip Scott Morrison (Apr 18 2021 at 11:28):

Or simply fork.


Last updated: May 14 2021 at 13:24 UTC