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