Looking for help with probability theory

Stream: new members

[Willem vanhulle]

Hi, I am a new user of Lean. As an exercise I tried demonstrating the Monty Hall problem using Bayes theorem from Mathlib4.

I reached a point were I or the AIs can't make any progress anymore. Could some help and have a look at my proof script?

The main problem I am struggling with is reducing infinite sums of probability densities. Please have a look :)

[Kenny Lau]

@Willem vanhulle why would you have an infinite sum when everything is finite?

[Willem vanhulle]

Kenny Lau zei:

Willem vanhulle why would you have an infinite sum when everything is finite?

I need it for creating a PMF I think.