From 7467c38b4f5f06ba5267031cc65a2b37d49d93e9 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Tue, 29 Jul 2025 15:53:59 +0200 Subject: [PATCH 1/3] Add comments to Bayesian monty --- RiddleProofs/MontyHall/MeasureTheory.lean | 4 +- RiddleProofs/MontyHall/Solution.lean | 227 +++++++++++++--------- RiddleProofs/MontyHall/Statement.lean | 14 +- 3 files changed, 146 insertions(+), 99 deletions(-) diff --git a/RiddleProofs/MontyHall/MeasureTheory.lean b/RiddleProofs/MontyHall/MeasureTheory.lean index 6a18528..e22d017 100644 --- a/RiddleProofs/MontyHall/MeasureTheory.lean +++ b/RiddleProofs/MontyHall/MeasureTheory.lean @@ -124,7 +124,9 @@ lemma comp_apply {Ω 𝓧 : Type*} [Fintype Ω] congr with ω exact CommMonoid.mul_comm ((κ ω) s) (μ {ω}) +/- Constructing a kernel from an arbitrary function requires measurability. A direct proof of measurability is much easier when the domain is countable. A measurable countable space with measurable singletons turns any function `f: α -> β` into a measurable function. -/ lemma Kernel.ofFunOfCountable_apply [MeasurableSpace α] [MeasurableSpace β] [Countable α] + /- `MeasurableSingletonClass is required when you need to evaluate kernel at a point. -/ [MeasurableSingletonClass α] (f : α → Measure β) (a : α) : Kernel.ofFunOfCountable f a = f a := rfl @@ -146,4 +148,4 @@ lemma sum_univ_of_three {α β : Type*} [Fintype α] [DecidableEq α] end Finset -end ProbabilityTheory \ No newline at end of file +end ProbabilityTheory diff --git a/RiddleProofs/MontyHall/Solution.lean b/RiddleProofs/MontyHall/Solution.lean index a63666c..e3a967d 100644 --- a/RiddleProofs/MontyHall/Solution.lean +++ b/RiddleProofs/MontyHall/Solution.lean @@ -33,78 +33,88 @@ instance subtype_ne_nonempty (p : Door) : Nonempty { d : Door // d ≠ p } := | .middle => ⟨⟨.left, by decide⟩⟩ | .right => ⟨⟨.left, by decide⟩⟩ -/-- likelihood kernel: if the car is at `p`, host picks uniformly among the two doors ≠ `p`. -/ -noncomputable def likelihood (p : Door) : Kernel CarLocation HostAction := - Kernel.ofFunOfCountable fun c => - if c = p then - -- host chooses uniformly on the two doors not equal to p - -- Map the measure from the subtype to Door - Measure.map (fun x : { d // d ≠ p } => x.val) - ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) +/-- Definition of a kernel representing conditional distributions of host actions given car locations. -/ +noncomputable def likelihood (picked : Door) : Kernel CarLocation HostAction := + /- A kernel κ : α -> Measure β assigns a measure on β for any a ∈ α. + In the context of probability theory, a is the value of a random variable X and κ(a) represents the conditional probability distribution of some random variable Y given X = a. -/ + Kernel.ofFunOfCountable fun car => + if car = picked then + -- host chooses uniformly on the two doors not equal to picked + -- Map the measure from the subtype to HostAction + let f : { d // d ≠ picked } → Door := λ x : { d // d ≠ picked } => x.val -- push-forward function + Measure.map f -- Computes push-forward of measure on codomain `HostAction`. + ((PMF.uniformOfFintype { d // d ≠ picked }).toMeasure) + -- `Measure.map` works by defining with the inverse map (f₊μ)(A) = μ(f⁻¹(A)). + -- _Remark_: `f` is not necessarily surjective, but should be measurable else - -- if car ≠ p, host must open the unique other door - (PMF.pure (other_door p c)).toMeasure - -instance (p : Door) : IsMarkovKernel (likelihood p) := -⟨fun c => by - by_cases hc : c = p + -- if car ≠ picked, host must open the unique other door + (PMF.pure (remaining_door picked car)).toMeasure + -- `PMF.pure` creates a PMF that assigns 1 to the singleton set `{remaining_door picked car}` + +/- The kernel `likelihood` must yield an actual probability measure for every `picked` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/ +instance (picked : Door) : IsMarkovKernel (likelihood picked) := +-- For any car location, we prove that `likelihood(picked)(car)` is a probability measure over `HostAction`. +⟨fun car => by + -- Consider each possible car location. + by_cases picked_eq_car : car = picked · -- uniform case: push-forward of a uniform PMF on the subtype - simp only [likelihood, hc, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) := - PMF.toMeasure.isProbabilityMeasure _ + show IsProbabilityMeasure ((likelihood picked) car) + simp only [likelihood, picked_eq_car, ProbabilityTheory.Kernel.ofFunOfCountable_apply] + -- We evaluate the kernel at `likelihood(picked)(car)` with `ofFunOfCountable_apply`. + haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ picked }).toMeasure) := + PMF.toMeasure.isProbabilityMeasure _ -- We can leave out `(PMF.uniformOfFintype { d // d ≠ picked })`. exact + -- If you push-forward a probability measure, it remains a probability measure. MeasureTheory.isProbabilityMeasure_map + /- Required condition: the push-forward function `f` is measurable. + A slightly more general version of measurability is "almost everywhere measurable" (`aemeasurable`). -/ measurable_subtype_coe.aemeasurable · -- deterministic case: `pure` PMF is a probability measure - simp only [likelihood, hc, ProbabilityTheory.Kernel.ofFunOfCountable_apply] + show IsProbabilityMeasure ((likelihood picked) car) + simp only [likelihood, picked_eq_car, ProbabilityTheory.Kernel.ofFunOfCountable_apply] + -- We evaluate the kernel at `likelihood(picked)(car)` with `ofFunOfCountable_apply`. exact PMF.toMeasure.isProbabilityMeasure _ ⟩ -/- Posterior kernel using Bayesian inference -/ -noncomputable def postK (p : Door) : Kernel HostAction CarLocation := - (likelihood p)†prior -section MontyHallBayes +/- The \dagger computes an application of the `posterior` operator on kernel `likelihood picked` with respect to prior distribution of cars in `prior`. + +It works by applying a generalized version of the Bayes theorem that reduces to the more familiar discrete form of Bayes' theorem: -lemma other_door_involutive {p h : Door} (h_ne_p : h ≠ p) : - other_door p (other_door p h) = h := by - cases p <;> cases h <;> simp [other_door] +P(Car=X | Host=Y) = P(Host=Y | Car=X) × P(Car=X) / P(Host=Y) -open scoped BigOperators +Where the marginal probability is computed like: + +P(Host=Y) = Σ_X P(Host=Y | Car=X) × P(Car=X) + +-/ +noncomputable def postK (p : Door) : Kernel HostAction CarLocation := + (likelihood p)†prior -lemma Door.card_eq_three : Fintype.card Door = 3 := by - decide lemma Fintype.card_subtype_ne_of_three (p : Door) : Fintype.card { d : Door // d ≠ p } = 2 := by rw [Fintype.card_subtype_compl, Door.card_eq_three] simp -namespace MontyHallBayes variable {p h : Door} (h_ne_p : h ≠ p) -/-- The third door, different from `p` and `h`. -/ -private noncomputable def o (p h : Door) : Door := - other_door p h -private lemma o_ne_p (p h : Door) (h_ne_p : h ≠ p) : o p h ≠ p := +private lemma remaining_ne_p (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ p := -- we use `h_ne_p.symm : p ≠ h` so that `other_door_is_other` matches its arguments (other_door_is_other (h_ne_p.symm)).1 -private lemma o_ne_h (p h : Door) (h_ne_p : h ≠ p) : o p h ≠ h := +private lemma remaining_ne_h (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ h := -- same trick (other_door_is_other (h_ne_p.symm)).2 private lemma other_door_of_ne {p h x : Door} (hp : p ≠ h) (hx_ne_p : x ≠ p) (hx_ne_h : x ≠ h) : - x = other_door p h := by + x = remaining_door p h := by revert p h x hp hx_ne_p hx_ne_h; decide variable {p h : Door} (h_ne_p : h ≠ p) -namespace Measure - -open scoped ENNReal /-- Probability that the push-forward of the uniform measure on the subtype @@ -112,9 +122,9 @@ Probability that the push-forward of the uniform measure on the subtype Since the subtype has exactly two elements, this value is `1 / 2`. -/ lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) : (Measure.map (fun x : { d // d ≠ p } => (x : Door)) + -- This lemma is only used when `pick = car` and the host has to choose uniformly between the two remaining doors. ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)) {h} = (1 : ℝ≥0∞) / 2 := by - classical have h_map : (Measure.map (fun x : { d // d ≠ p } => (x : Door)) ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)) {h} @@ -144,37 +154,37 @@ lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) : Fintype.card_unique, ENNReal.natCast_sub, Nat.cast_one, one_div, inv_inj, MeasurableSet.singleton] simp [h_map, h_pre, h_val] -end Measure -variable {p h : Door} (h_ne_p : h ≠ p) +variable {pick host : Door} -/-- If the car is behind door `p`, the host chooses uniformly among the two -remaining doors, so the probability that he opens `h ≠ p` is `1 / 2`. -/ -lemma likelihood_at_p (h_ne_p : h ≠ p) : - (likelihood p) p {h} = (1 : ℝ≥0∞) / 2 := by +/-- If the car is behind door `pick`, the host chooses uniformly among the two +remaining doors, so the probability that he opens `host ≠ pick` is `1 / 2`. -/ +lemma likelihood_host_opens_when_pick_car (h_ne_p : host ≠ pick) : + (likelihood pick) pick {host} = (1 : ℝ≥0∞) / 2 := by classical simpa [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - using Measure.map_uniform_subtype_singleton (p := p) (h := h) h_ne_p + using map_uniform_subtype_singleton (p := pick) (h := host) h_ne_p /-- If the car is behind door `h`, the host cannot open `h`. -/ -lemma likelihood_at_h (h_ne_p : h ≠ p) : - (likelihood p) h {h} = 0 := by - have h_ne : other_door p h ≠ h := (other_door_is_other h_ne_p.symm).2 - rw [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] +lemma likelihood_host_shows_car (h_ne_p : host ≠ pick) : + (likelihood pick) host {host} = 0 := by + have h_ne : remaining_door pick host ≠ host := (other_door_is_other h_ne_p.symm).2 + rw [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] -- Evaluate simple kernel. simp only [h_ne_p] - simp [PMF.pure_apply,] + simp [PMF.pure_apply,] -- Apply a PMF defined on a singleton set. exact id (Ne.symm h_ne) + /-- If the car is behind the third door `o p h`, the host must open `h`. -/ -lemma likelihood_at_o (h_ne_p : h ≠ p) : - (likelihood p) (o p h) {h} = 1 := by - have c_ne_p : o p h ≠ p := o_ne_p p h h_ne_p - have h_forced : other_door p (o p h) = h := by - rw [o, other_door_involutive h_ne_p] +lemma likelihood_host_door_not_pick_car (h_ne_p : host ≠ pick) : + (likelihood pick) (remaining_door pick host) {host} = 1 := by + have c_ne_p : remaining_door pick host ≠ pick := remaining_ne_p pick host h_ne_p + have h_forced : remaining_door pick (remaining_door pick host) = host := by + rw [other_door_involutive h_ne_p] rw [likelihood,ProbabilityTheory.Kernel.ofFunOfCountable_apply] simp only [c_ne_p] rw [h_forced] - have : (PMF.pure h).toMeasure {h} = 1 := by + have : (PMF.pure host).toMeasure {host} = 1 := by rw [PMF.toMeasure_apply_singleton] simp; exact trivial exact this @@ -183,23 +193,23 @@ open MeasureTheory ProbabilityTheory /-- The universe of doors consists of exactly the three doors `{p, h, o p h}`. -/ -lemma door_univ_eq_three (h_ne_p : h ≠ p) : - (Finset.univ : Finset Door) = {p, h, o p h} := by - ext x; simp; by_cases hxp : x = p; · left; assumption - right; by_cases hxh : x = h; · left; assumption +lemma door_univ_eq_three (h_ne_p : host ≠ pick) : + (Finset.univ : Finset Door) = {pick, host, remaining_door pick host} := by + ext x; simp; by_cases hxp : x = pick; · left; assumption + right; by_cases hxh : x = host; · left; assumption right; exact (other_door_of_ne h_ne_p.symm hxp hxh) /-- The three doors `p`, `h`, and `o p h` are pairwise distinct. -/ -lemma doors_pairwise_distinct (h_ne_p : h ≠ p) : - p ≠ h ∧ p ≠ o p h ∧ h ≠ o p h := by +lemma doors_pairwise_distinct (h_ne_p : host ≠ pick) : + pick ≠ host ∧ pick ≠ remaining_door pick host ∧ host ≠ remaining_door pick host := by constructor · exact h_ne_p.symm · constructor - · exact (o_ne_p p h h_ne_p).symm - · exact (o_ne_h p h h_ne_p).symm + · exact (remaining_ne_p pick host h_ne_p).symm + · exact (remaining_ne_h pick host h_ne_p).symm -/-- Each door has prior probability 1/3 under the uniform distribution. -/ -lemma prior_uniform (d : Door) : prior {d} = 1 / 3 := by +/-- Without host evidence, every door is equally likely to have car for participant. -/ +lemma eval_uniform_prior (d : Door) : prior {d} = 1 / 3 := by rw [prior] rw [PMF.toMeasure_apply_singleton (PMF.uniformOfFintype CarLocation) d] rw [PMF.uniformOfFintype_apply] @@ -207,46 +217,71 @@ lemma prior_uniform (d : Door) : prior {d} = 1 / 3 := by -/-- The marginal probability of the host opening door `h`. -/ -lemma marginal_prob_h (h_ne_p : h ≠ p) : - ((likelihood p) ∘ₘ prior) {h} = (1 : ℝ≥0∞) / 2 := by - classical + + +/- +First, it is important to understand the concept of the composition of a kernel with a measure. + +Given: +- μ : Measure α (a measure on space α) +- κ : Kernel α β (a kernel from α to β) + +The composition κ ∘ₘ μ : Measure β is defined as: +(κ ∘ₘ μ)(B) = ∫_{a ∈ α} κ(a)(B) dμ(a) +where κ(a)(B) is the measure that κ(a) assigns to set B ⊆ β + +In our Monty Hall context: +- α = CarLocation (the space/type) +- a ranges over specific car locations (door1, door2, door3) +- μ = prior (uniform measure on car locations) +- κ = likelihood pick (kernel giving host behavior for each car location) + +Integrate over all possible car locations, weighted by the prior probability of each location. + +-/ + + +/-- +What is the probability that the host will open door `host`. +-/ +lemma marginal_prob_h (h_ne_p : host ≠ pick) : + ((likelihood pick) ∘ₘ prior) {host} = (1 : ℝ≥0∞) / 2 := by + /- + We first apply a general measure-theoretic version of law of total probability `comp_apply`. In a discrete probability space this becomes: + Σ_car P(host opens | car location) × P(car location) + -/ rw [ProbabilityTheory.comp_apply _ _ (by simp)] have h_cover := door_univ_eq_three h_ne_p have h_doors_distinct := doors_pairwise_distinct h_ne_p rw [ProbabilityTheory.Finset.sum_univ_of_three _ h_doors_distinct.1 h_doors_distinct.2.1 h_doors_distinct.2.2 h_cover] - rw [likelihood_at_p h_ne_p, likelihood_at_h h_ne_p, likelihood_at_o h_ne_p] - rw [prior_uniform p, prior_uniform h, prior_uniform (o p h)] + -- Rewrite each term in the sum: + -- Case 1: Car at picked door → 1/3 × 1/2 + rw [likelihood_host_opens_when_pick_car h_ne_p, eval_uniform_prior pick] + -- Case 2: Car at host door → 1/3 × 0 + rw [likelihood_host_shows_car h_ne_p, eval_uniform_prior host] + -- Case 3: Car at remaining door → 1/3 × 1 + rw [likelihood_host_door_not_pick_car h_ne_p, eval_uniform_prior (remaining_door pick host)] eq_as_reals /- The probability of winning by switching doors. -/ theorem switch_wins_prob_bayes (p h : Door) (h_ne_p : h ≠ p) : - (postK p h) {other_door p h} = (2 : ℝ≥0∞) / 3 := by - classical - set o : Door := other_door p h with ho + (postK p h) {remaining_door p h} = (2 : ℝ≥0∞) / 3 := by + set o : Door := remaining_door p h with ho -- The denominator in Bayes’ formula is non-zero have hpos : ((likelihood p) ∘ₘ prior) {h} ≠ 0 := by rw [marginal_prob_h h_ne_p] norm_num -- Bayes’ rule specialised to singletons - have post_eq : - (postK p h) {o} = - (prior {o} * (likelihood p) o {h}) / - ((likelihood p) ∘ₘ prior) {h} := by - rw [postK] - exact posterior_apply_singleton (likelihood p) prior h o hpos - -- The prior is uniform - have prior_o : prior {o} = (1 : ℝ≥0∞) / 3 := by - simpa using prior_uniform o - have h_post : (postK p h) {o} = (2 : ℝ≥0∞) / 3 := by - have lik_o : (likelihood p) o {h} = 1 := by - simpa [ho] using likelihood_at_o (p := p) (h := h) h_ne_p - have : (prior {o} * (likelihood p) o {h}) / - ((likelihood p) ∘ₘ prior) {h} = (2 : ℝ≥0∞) / 3 := by - simp [prior_o, lik_o, marginal_prob_h h_ne_p, - div_eq_mul_inv, mul_comm] - simpa [post_eq] using this - simpa [ho] using h_post - -end MontyHallBayes + -- Direct calculation: (1/3 * 1) / (1/2) = 2/3 + calc (postK p h) {remaining_door p h} + = (postK p h) {o} := by rw [ho] + _ = (prior {o} * (likelihood p) o {h}) / ((likelihood p) ∘ₘ prior) {h} := by + rw [postK] + exact posterior_apply_singleton (likelihood p) prior h o hpos + _ = ((1 : ℝ≥0∞) / 3 * (likelihood p) o {h}) / ((1 : ℝ≥0∞) / 2) := by + rw [eval_uniform_prior, marginal_prob_h h_ne_p] + _ = ((1 : ℝ≥0∞) / 3 * 1) / ((1 : ℝ≥0∞) / 2) := by + rw [likelihood_host_door_not_pick_car h_ne_p] + _ = (2 : ℝ≥0∞) / 3 := by + eq_as_reals diff --git a/RiddleProofs/MontyHall/Statement.lean b/RiddleProofs/MontyHall/Statement.lean index c1e5c3f..21b91fa 100644 --- a/RiddleProofs/MontyHall/Statement.lean +++ b/RiddleProofs/MontyHall/Statement.lean @@ -51,7 +51,7 @@ instance : Nonempty Door := ⟨.left⟩ @[simp] -def other_door (d₁ d₂ : Door) : Door := +def remaining_door (d₁ d₂ : Door) : Door := if d₁ = d₂ then d₁ else match d₁, d₂ with | .left, .middle => .right @@ -63,8 +63,18 @@ def other_door (d₁ d₂ : Door) : Door := | _, _ => d₁ lemma other_door_is_other {d₁ d₂ : Door} (h : d₁ ≠ d₂) : - other_door d₁ d₂ ≠ d₁ ∧ other_door d₁ d₂ ≠ d₂ := by + remaining_door d₁ d₂ ≠ d₁ ∧ remaining_door d₁ d₂ ≠ d₂ := by revert d₁ d₂ h; decide abbrev CarLocation := Door abbrev HostAction := Door + + +lemma other_door_involutive {p h : Door} (h_ne_p : h ≠ p) : + remaining_door p (remaining_door p h) = h := by + cases p <;> cases h <;> simp [remaining_door] + + + +lemma Door.card_eq_three : Fintype.card Door = 3 := by + decide From f8ddbf36e41040846355c503b0c1606cb645396a Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Tue, 29 Jul 2025 16:08:43 +0200 Subject: [PATCH 2/3] Make naming more uniform --- RiddleProofs/MontyHall/Solution.lean | 131 +++++++++++++------------- RiddleProofs/MontyHall/Statement.lean | 2 - 2 files changed, 65 insertions(+), 68 deletions(-) diff --git a/RiddleProofs/MontyHall/Solution.lean b/RiddleProofs/MontyHall/Solution.lean index e3a967d..0395f62 100644 --- a/RiddleProofs/MontyHall/Solution.lean +++ b/RiddleProofs/MontyHall/Solution.lean @@ -15,6 +15,8 @@ open scoped ENNReal /-! ## Monty Hall Specific Definitions -/ +variable {p h c d : Door} + instance : StandardBorelSpace Door := inferInstance /- Prior: uniform on three doors (as a measure). -/ @@ -34,35 +36,35 @@ instance subtype_ne_nonempty (p : Door) : Nonempty { d : Door // d ≠ p } := | .right => ⟨⟨.left, by decide⟩⟩ /-- Definition of a kernel representing conditional distributions of host actions given car locations. -/ -noncomputable def likelihood (picked : Door) : Kernel CarLocation HostAction := +noncomputable def likelihood (p : Door) : Kernel CarLocation HostAction := /- A kernel κ : α -> Measure β assigns a measure on β for any a ∈ α. In the context of probability theory, a is the value of a random variable X and κ(a) represents the conditional probability distribution of some random variable Y given X = a. -/ - Kernel.ofFunOfCountable fun car => - if car = picked then - -- host chooses uniformly on the two doors not equal to picked + Kernel.ofFunOfCountable fun c => + if c = p then + -- host chooses uniformly on the two doors not equal to p -- Map the measure from the subtype to HostAction - let f : { d // d ≠ picked } → Door := λ x : { d // d ≠ picked } => x.val -- push-forward function + let f : { d // d ≠ p } → Door := λ x : { d // d ≠ p } => x.val -- push-forward function Measure.map f -- Computes push-forward of measure on codomain `HostAction`. - ((PMF.uniformOfFintype { d // d ≠ picked }).toMeasure) + ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) -- `Measure.map` works by defining with the inverse map (f₊μ)(A) = μ(f⁻¹(A)). -- _Remark_: `f` is not necessarily surjective, but should be measurable else - -- if car ≠ picked, host must open the unique other door - (PMF.pure (remaining_door picked car)).toMeasure - -- `PMF.pure` creates a PMF that assigns 1 to the singleton set `{remaining_door picked car}` - -/- The kernel `likelihood` must yield an actual probability measure for every `picked` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/ -instance (picked : Door) : IsMarkovKernel (likelihood picked) := --- For any car location, we prove that `likelihood(picked)(car)` is a probability measure over `HostAction`. -⟨fun car => by + -- if c ≠ p, host must open the unique other door + (PMF.pure (remaining_door p c)).toMeasure + -- `PMF.pure` creates a PMF that assigns 1 to the singleton set `{remaining_door p c}` + +/- The kernel `likelihood` must yield an actual probability measure for every `p` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/ +instance (p : Door) : IsMarkovKernel (likelihood p) := +-- For any car location, we prove that `likelihood(p)(c)` is a probability measure over `HostAction`. +⟨fun c => by -- Consider each possible car location. - by_cases picked_eq_car : car = picked + by_cases p_eq_c : c = p · -- uniform case: push-forward of a uniform PMF on the subtype - show IsProbabilityMeasure ((likelihood picked) car) - simp only [likelihood, picked_eq_car, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - -- We evaluate the kernel at `likelihood(picked)(car)` with `ofFunOfCountable_apply`. - haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ picked }).toMeasure) := - PMF.toMeasure.isProbabilityMeasure _ -- We can leave out `(PMF.uniformOfFintype { d // d ≠ picked })`. + show IsProbabilityMeasure ((likelihood p) c) + simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply] + -- We evaluate the kernel at `likelihood(p)(c)` with `ofFunOfCountable_apply`. + haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) := + PMF.toMeasure.isProbabilityMeasure _ -- We can leave out `(PMF.uniformOfFintype { d // d ≠ p })`. exact -- If you push-forward a probability measure, it remains a probability measure. MeasureTheory.isProbabilityMeasure_map @@ -70,14 +72,14 @@ instance (picked : Door) : IsMarkovKernel (likelihood picked) := A slightly more general version of measurability is "almost everywhere measurable" (`aemeasurable`). -/ measurable_subtype_coe.aemeasurable · -- deterministic case: `pure` PMF is a probability measure - show IsProbabilityMeasure ((likelihood picked) car) - simp only [likelihood, picked_eq_car, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - -- We evaluate the kernel at `likelihood(picked)(car)` with `ofFunOfCountable_apply`. + show IsProbabilityMeasure ((likelihood p) c) + simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply] + -- We evaluate the kernel at `likelihood(p)(c)` with `ofFunOfCountable_apply`. exact PMF.toMeasure.isProbabilityMeasure _ ⟩ -/- The \dagger computes an application of the `posterior` operator on kernel `likelihood picked` with respect to prior distribution of cars in `prior`. +/- The \dagger computes an application of the `posterior` operator on kernel `likelihood p` with respect to prior distribution of cars in `prior`. It works by applying a generalized version of the Bayes theorem that reduces to the more familiar discrete form of Bayes' theorem: @@ -97,25 +99,18 @@ lemma Fintype.card_subtype_ne_of_three (p : Door) : Fintype.card { d : Door // d rw [Fintype.card_subtype_compl, Door.card_eq_three] simp - -variable {p h : Door} (h_ne_p : h ≠ p) - - private lemma remaining_ne_p (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ p := - -- we use `h_ne_p.symm : p ≠ h` so that `other_door_is_other` matches its arguments + -- Use `h_ne_p.symm : p ≠ h` so that `other_door_is_other` matches its arguments (other_door_is_other (h_ne_p.symm)).1 private lemma remaining_ne_h (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ h := - -- same trick + (other_door_is_other (h_ne_p.symm)).2 private lemma other_door_of_ne {p h x : Door} (hp : p ≠ h) (hx_ne_p : x ≠ p) (hx_ne_h : x ≠ h) : x = remaining_door p h := by revert p h x hp hx_ne_p hx_ne_h; decide -variable {p h : Door} (h_ne_p : h ≠ p) - - /-- Probability that the push-forward of the uniform measure on the subtype `{d // d ≠ p}` assigns to the singleton `{h}`. @@ -155,36 +150,35 @@ lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) : simp [h_map, h_pre, h_val] -variable {pick host : Door} -/-- If the car is behind door `pick`, the host chooses uniformly among the two -remaining doors, so the probability that he opens `host ≠ pick` is `1 / 2`. -/ -lemma likelihood_host_opens_when_pick_car (h_ne_p : host ≠ pick) : - (likelihood pick) pick {host} = (1 : ℝ≥0∞) / 2 := by +/-- If the car is behind door `p`, the host chooses uniformly among the two +remaining doors, so the probability that he opens `h ≠ p` is `1 / 2`. -/ +lemma likelihood_at_when_part_pick_car (h_ne_p : h ≠ p) : + (likelihood p) p {h} = (1 : ℝ≥0∞) / 2 := by classical simpa [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - using map_uniform_subtype_singleton (p := pick) (h := host) h_ne_p + using map_uniform_subtype_singleton (p := p) (h := h) h_ne_p /-- If the car is behind door `h`, the host cannot open `h`. -/ -lemma likelihood_host_shows_car (h_ne_p : host ≠ pick) : - (likelihood pick) host {host} = 0 := by - have h_ne : remaining_door pick host ≠ host := (other_door_is_other h_ne_p.symm).2 +lemma likelihood_h_when_car_at_h (h_ne_p : h ≠ p) : + (likelihood p) h {h} = 0 := by + have h_ne : remaining_door p h ≠ h := (other_door_is_other h_ne_p.symm).2 rw [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] -- Evaluate simple kernel. simp only [h_ne_p] simp [PMF.pure_apply,] -- Apply a PMF defined on a singleton set. exact id (Ne.symm h_ne) -/-- If the car is behind the third door `o p h`, the host must open `h`. -/ -lemma likelihood_host_door_not_pick_car (h_ne_p : host ≠ pick) : - (likelihood pick) (remaining_door pick host) {host} = 1 := by - have c_ne_p : remaining_door pick host ≠ pick := remaining_ne_p pick host h_ne_p - have h_forced : remaining_door pick (remaining_door pick host) = host := by +/-- If the car is behind the third door `remaining_door p h`, the host must open `h`. -/ +lemma likelihood_at_h_when_part_not_pick_car (h_ne_p : h ≠ p) : + (likelihood p) (remaining_door p h) {h} = 1 := by + have c_ne_p : remaining_door p h ≠ p := remaining_ne_p p h h_ne_p + have h_forced : remaining_door p (remaining_door p h) = h := by rw [other_door_involutive h_ne_p] rw [likelihood,ProbabilityTheory.Kernel.ofFunOfCountable_apply] simp only [c_ne_p] rw [h_forced] - have : (PMF.pure host).toMeasure {host} = 1 := by + have : (PMF.pure h).toMeasure {h} = 1 := by rw [PMF.toMeasure_apply_singleton] simp; exact trivial exact this @@ -192,21 +186,21 @@ lemma likelihood_host_door_not_pick_car (h_ne_p : host ≠ pick) : open MeasureTheory ProbabilityTheory -/-- The universe of doors consists of exactly the three doors `{p, h, o p h}`. -/ -lemma door_univ_eq_three (h_ne_p : host ≠ pick) : - (Finset.univ : Finset Door) = {pick, host, remaining_door pick host} := by - ext x; simp; by_cases hxp : x = pick; · left; assumption - right; by_cases hxh : x = host; · left; assumption +/-- The universe of doors consists of exactly the three doors `{p, h, remaining_door p h}`. -/ +lemma door_univ_eq_three (h_ne_p : h ≠ p) : + (Finset.univ : Finset Door) = {p, h, remaining_door p h} := by + ext x; simp; by_cases hxp : x = p; · left; assumption + right; by_cases hxh : x = h; · left; assumption right; exact (other_door_of_ne h_ne_p.symm hxp hxh) -/-- The three doors `p`, `h`, and `o p h` are pairwise distinct. -/ -lemma doors_pairwise_distinct (h_ne_p : host ≠ pick) : - pick ≠ host ∧ pick ≠ remaining_door pick host ∧ host ≠ remaining_door pick host := by +/-- The three doors `p`, `h`, and `remaining_door p h` are pairwise distinct. -/ +lemma doors_pairwise_distinct (h_ne_p : h ≠ p) : + p ≠ h ∧ p ≠ remaining_door p h ∧ h ≠ remaining_door p h := by constructor · exact h_ne_p.symm · constructor - · exact (remaining_ne_p pick host h_ne_p).symm - · exact (remaining_ne_h pick host h_ne_p).symm + · exact (remaining_ne_p p h h_ne_p).symm + · exact (remaining_ne_h p h h_ne_p).symm /-- Without host evidence, every door is equally likely to have car for participant. -/ lemma eval_uniform_prior (d : Door) : prior {d} = 1 / 3 := by @@ -242,26 +236,31 @@ Integrate over all possible car locations, weighted by the prior probability of /-- -What is the probability that the host will open door `host`. +What is the probability that the host will open door `h`. -/ -lemma marginal_prob_h (h_ne_p : host ≠ pick) : - ((likelihood pick) ∘ₘ prior) {host} = (1 : ℝ≥0∞) / 2 := by +lemma marginal_prob_h (h_ne_p : h ≠ p) : + ((likelihood p) ∘ₘ prior) {h} = (1 : ℝ≥0∞) / 2 := by /- We first apply a general measure-theoretic version of law of total probability `comp_apply`. In a discrete probability space this becomes: - Σ_car P(host opens | car location) × P(car location) + Σ_car P(h opens | car location) × P(car location) -/ rw [ProbabilityTheory.comp_apply _ _ (by simp)] have h_cover := door_univ_eq_three h_ne_p have h_doors_distinct := doors_pairwise_distinct h_ne_p rw [ProbabilityTheory.Finset.sum_univ_of_three _ h_doors_distinct.1 h_doors_distinct.2.1 h_doors_distinct.2.2 h_cover] + show + prior {p} * ((likelihood p) p) {h} + + prior {h} * ((likelihood p) h) {h} + + prior {remaining_door p h} * ((likelihood p) (remaining_door p h)) {h} + = 1 / 2 -- Rewrite each term in the sum: -- Case 1: Car at picked door → 1/3 × 1/2 - rw [likelihood_host_opens_when_pick_car h_ne_p, eval_uniform_prior pick] + rw [likelihood_at_when_part_pick_car h_ne_p, eval_uniform_prior p] -- Case 2: Car at host door → 1/3 × 0 - rw [likelihood_host_shows_car h_ne_p, eval_uniform_prior host] + rw [likelihood_h_when_car_at_h h_ne_p, eval_uniform_prior h] -- Case 3: Car at remaining door → 1/3 × 1 - rw [likelihood_host_door_not_pick_car h_ne_p, eval_uniform_prior (remaining_door pick host)] + rw [likelihood_at_h_when_part_not_pick_car h_ne_p, eval_uniform_prior (remaining_door p h)] eq_as_reals /- The probability of winning by switching doors. -/ @@ -282,6 +281,6 @@ theorem switch_wins_prob_bayes (p h : Door) (h_ne_p : h ≠ p) : _ = ((1 : ℝ≥0∞) / 3 * (likelihood p) o {h}) / ((1 : ℝ≥0∞) / 2) := by rw [eval_uniform_prior, marginal_prob_h h_ne_p] _ = ((1 : ℝ≥0∞) / 3 * 1) / ((1 : ℝ≥0∞) / 2) := by - rw [likelihood_host_door_not_pick_car h_ne_p] + rw [likelihood_at_h_when_part_not_pick_car h_ne_p] _ = (2 : ℝ≥0∞) / 3 := by eq_as_reals diff --git a/RiddleProofs/MontyHall/Statement.lean b/RiddleProofs/MontyHall/Statement.lean index 21b91fa..1ae93b3 100644 --- a/RiddleProofs/MontyHall/Statement.lean +++ b/RiddleProofs/MontyHall/Statement.lean @@ -74,7 +74,5 @@ lemma other_door_involutive {p h : Door} (h_ne_p : h ≠ p) : remaining_door p (remaining_door p h) = h := by cases p <;> cases h <;> simp [remaining_door] - - lemma Door.card_eq_three : Fintype.card Door = 3 := by decide From 7065580897dd13c78bbc2e33a281e45201797020 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Tue, 29 Jul 2025 16:37:50 +0200 Subject: [PATCH 3/3] Improve comments --- RiddleProofs/MontyHall/MeasureTheory.lean | 4 +- RiddleProofs/MontyHall/Solution.lean | 58 +++++++++++------------ 2 files changed, 29 insertions(+), 33 deletions(-) diff --git a/RiddleProofs/MontyHall/MeasureTheory.lean b/RiddleProofs/MontyHall/MeasureTheory.lean index e22d017..4c9a295 100644 --- a/RiddleProofs/MontyHall/MeasureTheory.lean +++ b/RiddleProofs/MontyHall/MeasureTheory.lean @@ -3,8 +3,7 @@ import Mathlib.Probability.Kernel.Posterior /-! Written by Matteo Cipollina -This file contains generic measure theory, probability theory, and general Bayesian methods. -This includes all probability theory infrastructure that could be reused for other problems. +This file contains generic measure theory and probability theory. -/ set_option linter.unusedVariables false @@ -146,6 +145,7 @@ lemma sum_univ_of_three {α β : Type*} [Fintype α] [DecidableEq α] simp [Finset.sum_insert h₁, Finset.sum_insert h₂, Finset.sum_singleton, add_comm, add_left_comm] + end Finset end ProbabilityTheory diff --git a/RiddleProofs/MontyHall/Solution.lean b/RiddleProofs/MontyHall/Solution.lean index 0395f62..764cc91 100644 --- a/RiddleProofs/MontyHall/Solution.lean +++ b/RiddleProofs/MontyHall/Solution.lean @@ -19,7 +19,7 @@ variable {p h c d : Door} instance : StandardBorelSpace Door := inferInstance -/- Prior: uniform on three doors (as a measure). -/ +/-- Prior: uniform distribution on three doors (as a measure). -/ noncomputable def prior : Measure CarLocation := (PMF.uniformOfFintype CarLocation).toMeasure @@ -35,34 +35,35 @@ instance subtype_ne_nonempty (p : Door) : Nonempty { d : Door // d ≠ p } := | .middle => ⟨⟨.left, by decide⟩⟩ | .right => ⟨⟨.left, by decide⟩⟩ -/-- Definition of a kernel representing conditional distributions of host actions given car locations. -/ +/-- Definition of a kernel representing conditional distributions of host actions given car locations. + +A kernel κ : α → Measure β assigns a measure on β for any a ∈ α. +In the context of probability theory, a is the value of a random variable X and κ(a) represents the conditional probability distribution of some random variable Y given X = a. -/ noncomputable def likelihood (p : Door) : Kernel CarLocation HostAction := - /- A kernel κ : α -> Measure β assigns a measure on β for any a ∈ α. - In the context of probability theory, a is the value of a random variable X and κ(a) represents the conditional probability distribution of some random variable Y given X = a. -/ Kernel.ofFunOfCountable fun c => if c = p then - -- host chooses uniformly on the two doors not equal to p + -- Host chooses uniformly among the two doors not equal to p -- Map the measure from the subtype to HostAction - let f : { d // d ≠ p } → Door := λ x : { d // d ≠ p } => x.val -- push-forward function - Measure.map f -- Computes push-forward of measure on codomain `HostAction`. + let f : { d // d ≠ p } → Door := λ x : { d // d ≠ p } => x.val -- push-forward function + Measure.map f -- Computes push-forward of measure on codomain `HostAction` ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) - -- `Measure.map` works by defining with the inverse map (f₊μ)(A) = μ(f⁻¹(A)). - -- _Remark_: `f` is not necessarily surjective, but should be measurable + -- `Measure.map` works by defining the inverse map (f₊μ)(A) = μ(f⁻¹(A)) + -- Remark: `f` is not necessarily surjective, but should be measurable else - -- if c ≠ p, host must open the unique other door + -- If c ≠ p, host must open the unique other door (PMF.pure (remaining_door p c)).toMeasure - -- `PMF.pure` creates a PMF that assigns 1 to the singleton set `{remaining_door p c}` + -- `PMF.pure` creates a PMF that assigns probability 1 to the singleton set `{remaining_door p c}` -/- The kernel `likelihood` must yield an actual probability measure for every `p` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/ +/-- The kernel `likelihood` must yield an actual probability measure for every `p` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/ instance (p : Door) : IsMarkovKernel (likelihood p) := --- For any car location, we prove that `likelihood(p)(c)` is a probability measure over `HostAction`. +-- For any car location, we prove that `likelihood p c` is a probability measure over `HostAction`. ⟨fun c => by -- Consider each possible car location. by_cases p_eq_c : c = p · -- uniform case: push-forward of a uniform PMF on the subtype show IsProbabilityMeasure ((likelihood p) c) simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - -- We evaluate the kernel at `likelihood(p)(c)` with `ofFunOfCountable_apply`. + -- We evaluate the kernel at `likelihood p c` with `ofFunOfCountable_apply`. haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) := PMF.toMeasure.isProbabilityMeasure _ -- We can leave out `(PMF.uniformOfFintype { d // d ≠ p })`. exact @@ -74,18 +75,18 @@ instance (p : Door) : IsMarkovKernel (likelihood p) := · -- deterministic case: `pure` PMF is a probability measure show IsProbabilityMeasure ((likelihood p) c) simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply] - -- We evaluate the kernel at `likelihood(p)(c)` with `ofFunOfCountable_apply`. + -- We evaluate the kernel at `likelihood p c` with `ofFunOfCountable_apply`. exact PMF.toMeasure.isProbabilityMeasure _ ⟩ -/- The \dagger computes an application of the `posterior` operator on kernel `likelihood p` with respect to prior distribution of cars in `prior`. +/-- The † operator computes an application of the `posterior` operator on kernel `likelihood p` with respect to prior distribution of cars in `prior`. -It works by applying a generalized version of the Bayes theorem that reduces to the more familiar discrete form of Bayes' theorem: +It works by applying a generalized version of Bayes' theorem that reduces to the more familiar discrete form of Bayes' theorem: P(Car=X | Host=Y) = P(Host=Y | Car=X) × P(Car=X) / P(Host=Y) -Where the marginal probability is computed like: +Where the marginal probability is computed as: P(Host=Y) = Σ_X P(Host=Y | Car=X) × P(Car=X) @@ -117,7 +118,7 @@ Probability that the push-forward of the uniform measure on the subtype Since the subtype has exactly two elements, this value is `1 / 2`. -/ lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) : (Measure.map (fun x : { d // d ≠ p } => (x : Door)) - -- This lemma is only used when `pick = car` and the host has to choose uniformly between the two remaining doors. + -- This lemma is only used when `p = c` and the host has to choose uniformly between the two remaining doors. ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)) {h} = (1 : ℝ≥0∞) / 2 := by have h_map : @@ -228,22 +229,18 @@ In our Monty Hall context: - α = CarLocation (the space/type) - a ranges over specific car locations (door1, door2, door3) - μ = prior (uniform measure on car locations) -- κ = likelihood pick (kernel giving host behavior for each car location) +- κ = likelihood p (kernel giving host behavior for each car location) Integrate over all possible car locations, weighted by the prior probability of each location. -/ -/-- -What is the probability that the host will open door `h`. --/ +/-- What is the probability that the host will open door `h`? -/ lemma marginal_prob_h (h_ne_p : h ≠ p) : ((likelihood p) ∘ₘ prior) {h} = (1 : ℝ≥0∞) / 2 := by - /- - We first apply a general measure-theoretic version of law of total probability `comp_apply`. In a discrete probability space this becomes: - Σ_car P(h opens | car location) × P(car location) - -/ + -- We first apply a general measure-theoretic version of the law of total probability `comp_apply`. In a discrete probability space this becomes: + -- Σ_car P(host opens h | car location) × P(car location) rw [ProbabilityTheory.comp_apply _ _ (by simp)] have h_cover := door_univ_eq_three h_ne_p have h_doors_distinct := doors_pairwise_distinct h_ne_p @@ -263,20 +260,19 @@ lemma marginal_prob_h (h_ne_p : h ≠ p) : rw [likelihood_at_h_when_part_not_pick_car h_ne_p, eval_uniform_prior (remaining_door p h)] eq_as_reals -/- The probability of winning by switching doors. -/ +/-- The probability of winning by switching doors. -/ theorem switch_wins_prob_bayes (p h : Door) (h_ne_p : h ≠ p) : (postK p h) {remaining_door p h} = (2 : ℝ≥0∞) / 3 := by set o : Door := remaining_door p h with ho -- The denominator in Bayes’ formula is non-zero have hpos : ((likelihood p) ∘ₘ prior) {h} ≠ 0 := by rw [marginal_prob_h h_ne_p] - norm_num - -- Bayes’ rule specialised to singletons - -- Direct calculation: (1/3 * 1) / (1/2) = 2/3 + eq_as_reals calc (postK p h) {remaining_door p h} = (postK p h) {o} := by rw [ho] _ = (prior {o} * (likelihood p) o {h}) / ((likelihood p) ∘ₘ prior) {h} := by rw [postK] + -- Bayes’ rule specialised to singletons exact posterior_apply_singleton (likelihood p) prior h o hpos _ = ((1 : ℝ≥0∞) / 3 * (likelihood p) o {h}) / ((1 : ℝ≥0∞) / 2) := by rw [eval_uniform_prior, marginal_prob_h h_ne_p]