# Zulip Chat Archive

## Stream: new members

### Topic: Probability theory

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

#### Bryan Gin-ge Chen (Apr 03 2021 at 23:03):

(I've renamed the thread.)

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

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

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

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

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

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

#### Mario Carneiro (Apr 17 2021 at 16:32):

That's what I just said

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

#### Mario Carneiro (Apr 17 2021 at 16:35):

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

#### Mario Carneiro (Apr 17 2021 at 16:35):

but you can have constructors for both versions

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

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

#### Scott Morrison (Apr 18 2021 at 11:28):

Or simply fork.

Last updated: May 14 2021 at 13:24 UTC