Bayes theorem in Monty Hall problem

Stream: mathlib4

[Willem vanhulle]

I have created a statement of the Monty Hall brain teaser and proved some parts, but I am still stick with most of the proofs. Could someone help me to advance a little bit?

I mainly don't know how to reduce the created measure and calculate probabilities.

The code is on this PR https://github.com/wvhulle/riddle-proofs/pull/1.

[Willem vanhulle]

I got a little further, but probably I am doing something over-complicated

noncomputable def P  := p.toMeasure



-- door 1 has a car behind it
def H : Set MontyOutcome :=
  { ω | ω.car = 1 }

-- evidence that Monty has revealed a door with a goat behind it
def E : Set MontyOutcome :=
  { ω | ω.pick = 1 ∧ ω.car ≠ 1 }

-- Prior probability that door 1 has the car
example : P H = 1 / 3 := by
  sorry

example : P[H|E] = 2 / 3 := by
  have : MeasurableSet H := by sorry
  have: MeasurableSet E := by sorry
  have : IsFiniteMeasure P := by sorry
  rw [cond_eq_inv_mul_cond_mul _ _ P]
  sorry

[Willem vanhulle]

Can someone help me computing the probabilities of discrete events in a finite event space? It is kind of blocking me. I don't know how to actually compute things like Prob H where Prob is a probability measure and H is an event, eventhough H is one of the finite amount of events.

def H := { ω : ShowOutcome | ω.pick = left ∧ ω.car = left}

The source code is here.

[Michael Rothgang]

Have you seen https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ already?

[Rémy Degenne]

That blog post does not say anything about actually computing probabilities in finite probability spaces. It's all about how to start doing probability theory with generic distributions.

[Willem vanhulle]

Michael Rothgang zei:

Have you seen https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ already?

Yes I read it. It did not answer all my questions.

[metakuntyyy]

Maybe this will help you. It uses concrete calculations.
https://leanprover-community.github.io/mathlib4_docs/Archive/Wiedijk100Theorems/BirthdayProblem.html#Theorems100.birthday_measure