## Stream: new members

### Topic: probability and sets?

#### Miraç Gülgönül (Nov 18 2020 at 12:28):

Hello everyone, I am an engineering student fascinated by "digitizing" mathematics and a lean newbie. I was wondering if there was any way in lean to prove basic probability identities like say $P(A \cup B) \leq P(A) + P(B)$. I'm suspecting this requires formalizing the $P()$ probability law using measure theory or something, which I have no idea about :)

#### Patrick Massot (Nov 18 2020 at 12:51):

We don't have much probability theory in mathlib, but we don't have some measure theory. For instance your statement is docs#measure_theory.measure_union_le

#### Miraç Gülgönül (Nov 18 2020 at 13:08):

thanks! could you also give me an example on how to implement this :sweat_smile: ? how do I construct [measurable_space α] {μ : measure_theory.measure α} ? For example like in a file:

import data.set
import measure_theory.measure_space

open set

variable {U : Type}
variables A B C : set U
variable x : U

????


#### Kevin Buzzard (Nov 18 2020 at 13:13):

import measure_theory.measure_space

open measure_theory

variables {U : Type} [measurable_space U]
variable {μ : measure U}
variables A B : set U

example : μ (A ∪ B) ≤ μ A + μ B :=
begin
apply measure_union_le,
end


#### Miraç Gülgönül (Nov 18 2020 at 14:34):

final question :D apparently one can define this measure to be a docs#measure_theory.probability_measure, but I couldn't figure out how to "instantiate" it. How do I assert that $\mu$ is a probability_measure ?

#### Kevin Buzzard (Nov 18 2020 at 14:56):

Probably just add [probability_measure \mu] after {\mu : measure U}?

#### Miraç Gülgönül (Nov 18 2020 at 16:30):

that works! however a minor inconvenience, now the assumptions measurable_space U and probability_measure P have ugly names like _inst_1 and _inst_2. Can I alias these somehow ? I have tried

variables {U : Type}
variable ms : measurable_space U

variables {P : measure U}
variable pm : probability_measure P

variables A B : set U

example : P (A ∪ B) ≤ P A + P B :=
begin
apply measure_union_le,
end


but this causes the probability_measure P to dissappear from the state, it only shows:

U: Type
ms: measurable_space U
P: measure U
A B: set U
⊢ ⇑P (A ∪ B) ≤ ⇑P A + ⇑P B


#### Reid Barton (Nov 18 2020 at 16:33):

It's better to leave the default names (note that you didn't need to refer to them by name to apply measure_union_le).

#### Reid Barton (Nov 18 2020 at 16:34):

In math you would also say "Let U be a measurable space and P a probability measure on U" and not have a specific name for the hypothesis that U is a measurable space and so on.

#### Reid Barton (Nov 18 2020 at 16:34):

But if you really want you can force them to be included by writing include ms pm somewhere before example.

#### Miraç Gülgönül (Nov 18 2020 at 16:36):

thanks for the insight!

#### Kevin Buzzard (Nov 18 2020 at 17:57):

The idea is that if something is a typeclass then the system should be able to supply the variables with ugly names, and the human should never need to explicitly refer to them. In Lean functions have three kinds of input: round brackets (), meaning "user supplies them", squiggly brackets {} meaning "system will figure them out from the types of other inputs, and square bracket [] inputs, meaning "system will figure them out by looking at a database of instances, so don't worry that they have horrible names, you should never need to use them".

#### Miraç Gülgönül (Nov 18 2020 at 18:24):

but then how I would "use" the fact that the measure $P$ is indeed a "probability" measure ? for example right now I am doing:

import measure_theory.measure_space

noncomputable theory
open measure_theory set

variables {P : measure ℕ} [probability_measure P]
variables {A B : set ℕ}

/- 3.(Normalization)
The probability of the entire sample space Ω is equal to 1, that is,P(Ω) = 1.
-/
lemma normalization : P(univ) = 1 :=
begin
--simp
end


I was hoping I would be able to simp it away, since the lemma is literally the definition of the probability_measure class, however I don't seem to be able to extract it.

#### Kevin Buzzard (Nov 18 2020 at 18:25):

lemma normalization : P(univ) = 1 :=
begin
exact probability_measure.measure_univ
end


#### Kevin Buzzard (Nov 18 2020 at 18:31):

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


This (from mathlib) defines (amongst other things) a function probability_measure.measure_univ.

#check @probability_measure.measure_univ
/-
measure_univ :
∀ {α : Type u_1} [_inst_1 : measurable_space α] {μ : measure α}
[c : probability_measure μ], ⇑μ univ = 1
-/


The function says "I'll guess alpha and the fact that it's a measurable space, I'll guess mu, I'll guess the fact that mu is a probability measure, and I will output a proof that mu(univ)=1. If you attempt to use me on a goal which looks like P univ = 1, I will guess mu = P, P is a measure on nat so I'll guess alpha is nat, and now I'll look in my database of instances (square bracket stuff) to find the other things."

#### Miraç Gülgönül (Nov 18 2020 at 18:33):

I kept thinking it had to be something like P.measure_univ, it seems to me like the expression probability_measure.measure_univ suggests that it has nothing to do with P itself: but of course your explanation makes sense :D I should do more reading on classes/instances on lean!

#### Kevin Buzzard (Nov 18 2020 at 18:34):

Dot notation unfortunately won't work here, in fact that was the first thing I tried, but P : measure nat so P.measure_univ expands to measure.measure_univ P rather than probability_measure.measure_univ, that's why it doesn't work here.

Last updated: May 08 2021 at 10:12 UTC