# Zulip Chat Archive

## Stream: triage

### Topic: PR #5574: feat(archive/100-theorems-list): Ballot Problem

#### Random Issue Bot (Jan 22 2021 at 14:53):

Today I chose PR 5574 for discussion!

**feat(archive/100-theorems-list): Ballot Problem**

Created by @Bhavik Mehta (@b-mehta) on 2021-01-02

Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Bhavik Mehta (Jan 22 2021 at 19:17):

I haven't really looked at this in a while - the primary sticking point is that it defines a probability on finsets in a naive way:

```
/-- `Prob s P` is the probability that a random element from `s` satisfies the predicate `P`. -/
def Prob {α : Type*} (s : finset α) (P : α → Prop) [decidable_pred P] : ℚ :=
(s.filter P).card / s.card
```

which is good enough to state and prove the ballot problem, but not really much else of any interest; and isn't linked to the measure theory library. I was thinking about extending it to non-uniform but finite sample spaces which would be enough to do a big portion of probabilistic combinatorics (in particular probabilistic graph theory) but it basically just was the same as weighted sums and center mass in mathlib already so I pretty quickly stopped. At some point I'd like to get back to this and create API for probabilistic combinatorics, possibly moving `finset.center_mass`

out of `analysis/convex/basic`

and adapting `measure_theory/probability_mass_function`

. The sort of API I have in mind would have a structure `finite_probability_space`

containing a finite sample space and a pmf on it, and functions to express the probability of an event and the expectation of a function on it. One of the important things it would need is a definition of the space `G(n,p)`

of graphs with n vertices and each edge present independently with probability `p`

- obviously this is just the product measure of `n choose 2`

bernoulli variables but it's not obvious to me that you can build the resultant probability space to explicitly have its sample space as graphs on n vertices. Perhaps the people who've thought about measure theory and probability theory in Lean can weigh in?

#### Bhavik Mehta (Jan 22 2021 at 19:20):

As a concrete example, let X be the number of triangles in a graph from G(n,p), then I'd like to show that E[X] is `(n choose 3) * p^3`

and the variance of X is `<= n^3 p^3 + n^4 p^5`

(if it matters, specifically `(n choose 3) (p^3 - p^6) + (n choose 3) * 3 * (n - 3) * (p^5 - p^6)`

#### Heather Macbeth (Jan 22 2021 at 19:26):

Maybe @Rémy Degenne, who started probability theory in mathlib literally today (#5848), has some ideas.

#### Heather Macbeth (Jan 22 2021 at 19:28):

(Maybe that's a slight exaggeration, `measure_theory/probability_mass_function`

already exists as you noted.)

#### Heather Macbeth (Jan 22 2021 at 19:30):

Is your sample space the same as `(size-2 subsets of fin n) → Prop`

? Can you use the product measure on this, from Floris' work? (if that's not overkill).

#### Heather Macbeth (Jan 22 2021 at 19:31):

where the measure on `Prop`

is `p`

for true, `1 - p`

for false.

#### Bhavik Mehta (Jan 22 2021 at 19:47):

I don't think this is overkill, but my concern is that doing it like that could be awkward to work with in practice - `(size-2 subsets of fin n) -> Prop`

is ultimately the same thing as the sample space I want, but doing the translation in Lean of probability spaces to one on `simple_graph (fin n)`

feels like it could get painful?

#### Heather Macbeth (Jan 22 2021 at 20:04):

Maybe it works to make the structure "internal" ... here's one idea: Define a measure on a finite Boolean algebra by giving each atom `i`

a probability `p_i`

, and then make the measure of any other element the product of `p_i`

for each atom less than it with `(1 - p_i)`

for each atom not less than it. Then, put a Boolean algebra structure on `simple_graph (fin n)`

, where `≤`

means the edges of the first are contained in the edges of the second.

#### Heather Macbeth (Jan 22 2021 at 20:06):

The math here is completely untested, but you get the idea. Another way would be (if we have "internal" direct products yet) to put an internal direct product structure on `simple_graph (fin n)`

, allowing you to realize the `(size-2 subsets of fin n) → Prop`

idea "from the inside".

#### Random Issue Bot (Apr 01 2021 at 14:24):

Today I chose PR 5574 for discussion!

**feat(archive/100-theorems-list): Ballot Problem**

Created by @Bhavik Mehta (@b-mehta) on 2021-01-02

Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

Last updated: May 09 2021 at 16:20 UTC