probability and sets?

Stream: new members

[Miraç Gülgönül]

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]

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]

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]

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]

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]

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

[Miraç Gülgönül]

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]

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]

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]

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]

thanks for the insight!

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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.