Calculating probability proving optimal strategy Monty Hall

Stream: mathlib4

[Willem vanhulle]

Hi, I am in the final stages of the proof. Three sorries are remaining.

Given these definitions:

set H := car_at left
set E := pick_door left ∩ host_opens right ∪ pick_door left ∩ host_opens middle

I don't know how to calculate these probabilities:

Prob (H ∩ E) = 1 / 3
Prob H   = 1/3

Maybe someone with knowledge about the API of the uniform probability density in Mathlib4 has an idea about which tactic I should use?

The full code is here.

[Matteo Cipollina]

Willem vanhulle ha scritto:

Hi, I am in the final stages of the proof. Three sorries are remaining.

Given these definitions:

set H := car_at left
set E := pick_door left ∩ host_opens right ∪ pick_door left ∩ host_opens middle

I don't know how to calculate these probabilities:

Prob (H ∩ E) = 1 / 3
Prob H   = 1/3

Maybe someone with knowledge about the API of the uniform probability density in Mathlib4 has an idea about which tactic I should use?

The full code is here.

I think there is an issue in the file: you are counting outcomes combinatorially - in a space of all possible game histories - instead of using Bayesian Inference, ie update a prior belief with new information. eg PMF.uniformOfFinset valid_games_finset assumes that every valid game history is equally likely, which is not true.

[Willem vanhulle]

Yes, I noticed that as well. I will push the previous version instead which some more decision logic.

I guess this would be better?

def game_weight (ω : Game) : ℝ :=
  if ω.host = ω.pick then 0     -- Host never opens the picked door.
  else if ω.host = ω.car then 0 -- Host never opens the car door.
  else
    if ω.car = ω.pick then 1    -- Contestant chose the car. Host chooses from 2 doors.
    else 2                      -- Contestant chose a goat. Host is forced to open the only other goat door.

[Matteo Cipollina]

that seems correct, though I'd still use a more bayesian approach, where the sample space is only the unknown state of the world, and information is used to update beliefs about that state, and where the host is modeled by a likelihood function, rather than a weighting function. It's a more general approach that can be extended to continuous scenarios and handle better more complex sample space (where your approach can become unwiely for more complex problems) . But your approach with this revised defintion should work too

[Willem vanhulle]

Matteo Cipollina zei:

I'd still use a more bayesian approach, where the sample space is only the unknown state of the world, and information is used to update beliefs about that state, and where the host is modeled by a likelihood function, rather than a weighting function. It's a more general approach that can be extended to continuous scenarios and handle better more complex sample space (where your approach can become unwiely for more complex problems) . But your approach with this revised defintion should work too

Ah, well I haven't really used the Bayesian approach yet. Do you recommend learning about it directly trying to apply it? I have trouble computing the probability of the winning strategy.

[Willem vanhulle]

Is my impression correct that this part of Lean (probability theory, Bayesian statistics) is not very developped?

[Matteo Cipollina]

Willem vanhulle ha scritto:

Is my impression correct that this part of Lean (probability theory, Bayesian statistics) is not very developped?

Not directly developed, but you can find most of general tools needed to model a theory of conditional probability built on kernels and measure theory , and with it to build the Bayesian update you need.

[Willem vanhulle]

Could you help me with the first steps? Or maybe give a reference that I could read?

[Willem vanhulle]

I spent a week on this problem already on the classical approach (which I can show).

[Willem vanhulle]

I almost have the full proof for the Monty Hall dilemma but started doubting my model again. For some reason Prob[host_opens host | (car_at pick)ᶜ] = 1/2 does not hold. Instead Prob[host_opens host | (car_at pick)ᶜ] = 1/4 which breaks the main theorem.

Does anyone know what I did wrong? Did I use the wrong assumptions or model?

Source code: GitHub

[Matteo Cipollina]

it seems your lean code and 1/4 outcome is correct within your model, but your model does not represent the correct sample space and probability measure of the actual scenario. If I understand correctly, for the sample space you assume  the set of all possible valid final states (car, pick, host), and assume that each of those tuples is equally likely. But the sample space Ω should be based on the initial, random events: the car location and player's initial choice, which are independent and uniform. The host's choice is a function that depends on the outcome (car, choice) ∈ Ω

[Willem vanhulle]

@Matteo Cipollina, oh thanks! So you would recommend removing host as a field from the Game structure? How can I condition at the end on the pick of the host after the hosts decision is not anymore a field of the Game structure?

[Matteo Cipollina]

I've made a PR to your repo with the Bayesian version of Monty Hall, leveraging the Kernel.Posterior.lean in mathlib (adapted to singletons). While unneccesarily powerful for this 'simple' combiantorial problem, I think it is the most general, elegant and interesting way to frame it mathematically. The framework can be easily adapted to much more complex real-world problems, by varying the sample space (eg non Uniform), likelihood function etc. I think it can help you understand how Bayesian inference can work in real practice in lean and how to better frame your combinatorial formalization, so you can have both in the repo :)

https://github.com/wvhulle/learn-lean-riddles/pull/26/files

[Willem vanhulle]

@Matteo Cipollina Wow! Thanks! I was struggling with this problem for weeks, so this is very helpful of you :). I'll have a look at it.