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

Stream: triage

[Random Issue Bot]

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]

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]

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]

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

[Heather Macbeth]

(Maybe that's a slight exaggeration, measure_theory/probability_mass_function already exists as you noted.)

[Heather Macbeth]

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]

where the measure on Prop is p for true, 1 - p for false.

[Bhavik Mehta]

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]

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]

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]

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?

[Random Issue Bot]

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, please-adopt

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

[Ruben Van de Velde]

Hmm, this has some probability stuff, like:

/-- `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

Do we have things like that in mathlib by now?

[Bhavik Mehta]

Not that I know of, perhaps @Heather Macbeth or @Jason KY. will know better! As I mentioned in the past, the probability stuff which I did here in a very ad-hoc way is the primary objection to merging this (in my view, at least)