From a851a0800576f028ea810f53dd69ee0f4a5de779 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 3 Oct 2026 23:29:07 -0400 Subject: [PATCH 1/5] feat(Probability): add real-valued sums and event probabilities for PMFs Adds general lemmas to `Cslib.Probability.PMF` for working with real-valued masses. The masses of any PMF are summable and sum to one (`tsum_toReal`, `sum_toReal`), the mass of an outcome of `PMF.bind` is the weighted average of the conditional masses (`bind_apply_toReal_tsum`, `bind_apply_toReal`), and expectations of real-valued scores transform as expected under `map`, `bind`, and affine maps. For events, it adds the bounds `toOuterMeasure_le_one` and `toOuterMeasure_ne_top`, complements, positivity, the real-valued form of conditioning with `PMF.filter`, and the law of total probability for `PMF.bind`. These are the PMF facts used by the statistical distance and security-game PRs that follow. Like the rest of the module, they are domain-independent and candidates for Mathlib. --- Cslib/Probability/PMF.lean | 124 +++++++++++++++++++++++++++++++++++++ 1 file changed, 124 insertions(+) diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index af21c67c9..58a57c7a2 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -80,6 +80,130 @@ theorem uniformOfFintype_apply [Fintype α] [Nonempty α] (a : α) : uniformOfFintype α a = (Fintype.card α : ℝ≥0∞)⁻¹ := by simp [uniformOfFintype] +/-- Real-valued probability masses are summable, even on an infinite ambient type. -/ +theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) := + ENNReal.summable_toReal p.tsum_coe_ne_top + +/-- The real-valued masses of any discrete distribution sum to one. -/ +@[simp] theorem tsum_toReal (p : PMF α) : ∑' a, (p a).toReal = 1 := by + rw [← ENNReal.tsum_toReal_eq p.apply_ne_top, p.tsum_coe, ENNReal.toReal_one] + +/-- The real-valued probabilities of a finite distribution sum to one. -/ +theorem sum_toReal [Fintype α] (p : PMF α) : + ∑ a, (p a).toReal = 1 := by simpa only [tsum_fintype] using tsum_toReal p + +/-- An event has probability at most one. -/ +theorem toOuterMeasure_le_one (p : PMF α) (event : Set α) : p.toOuterMeasure event ≤ 1 := by + rw [PMF.toOuterMeasure_apply, ← p.tsum_coe] + exact ENNReal.tsum_le_tsum (fun a => Set.indicator_apply_le (fun _ => le_rfl)) + +/-- The probability of any event is finite. -/ +theorem toOuterMeasure_ne_top (p : PMF α) (event : Set α) : p.toOuterMeasure event ≠ ⊤ := + ne_of_lt ((toOuterMeasure_le_one p event).trans_lt ENNReal.one_lt_top) + +open Classical in +/-- Event probabilities on finite spaces are sums of the masses of their members. -/ +theorem toOuterMeasure_apply_toReal [Fintype α] (p : PMF α) (event : Set α) : + (p.toOuterMeasure event).toReal = ∑ a, if a ∈ event then (p a).toReal else 0 := by + rw [PMF.toOuterMeasure_apply_fintype, ENNReal.toReal_sum] + · apply Finset.sum_congr rfl + intro a _ + by_cases ha : a ∈ event <;> simp [ha] + · intro a _ + by_cases ha : a ∈ event <;> simp [ha, PMF.apply_ne_top] + +/-- An event and its complement have total probability one, in real-valued probability units. -/ +theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : + (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1 := by + have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by + rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] + convert p.tsum_coe using 1 + congr 1 + funext a + by_cases ha : a ∈ event <;> simp [ha] + simpa only [ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _), + ENNReal.toReal_one] using congrArg ENNReal.toReal h + +/-- An event has positive real probability exactly when it contains a possible outcome. -/ +theorem toOuterMeasure_toReal_pos_iff (p : PMF α) (event : Set α) : + 0 < (p.toOuterMeasure event).toReal ↔ ∃ a ∈ event, a ∈ p.support := by + classical + simp [ENNReal.toReal_pos_iff, lt_top_iff_ne_top, toOuterMeasure_ne_top, pos_iff_ne_zero, + PMF.toOuterMeasure_apply_eq_zero_iff, Set.disjoint_left, and_comm] + +open Classical in +/-- Conditioning keeps the event's masses and divides them by its probability. -/ +theorem filter_apply_toReal (p : PMF α) (event : Set α) + (hevent : ∃ a ∈ event, a ∈ p.support) (a : α) : + ((p.filter event hevent) a).toReal = + if a ∈ event then (p a).toReal / (p.toOuterMeasure event).toReal else 0 := by + rw [PMF.filter_apply, ← PMF.toOuterMeasure_apply] + by_cases ha : a ∈ event <;> simp [ha, ENNReal.toReal_mul, div_eq_mul_inv] + +/-- Event probability after a finite random choice is the average conditional probability. -/ +theorem toOuterMeasure_bind_toReal [Fintype α] (p : PMF α) (kernel : α → PMF β) + (event : Set β) : + ((p.bind kernel).toOuterMeasure event).toReal = + ∑ a, (p a).toReal * ((kernel a).toOuterMeasure event).toReal := by + rw [PMF.toOuterMeasure_bind_apply, tsum_fintype, ENNReal.toReal_sum + (fun a _ => ENNReal.mul_ne_top (PMF.apply_ne_top _ _) (toOuterMeasure_ne_top _ _))] + simp only [ENNReal.toReal_mul] + +/-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/ +theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) : + (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by + rw [PMF.bind_apply, ENNReal.tsum_toReal_eq (fun a => + ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b))] + simp only [ENNReal.toReal_mul] + +/-- The probability of an outcome after a finite random choice is its weighted average. -/ +theorem bind_apply_toReal [Fintype α] (p : PMF α) + (kernel : α → PMF β) (b : β) : + (p.bind kernel b).toReal = + ∑ a, (p a).toReal * (kernel a b).toReal := by + simpa only [tsum_fintype] using bind_apply_toReal_tsum p kernel b + +/-- The mass of a deterministic image is the sum of the masses in its fiber. -/ +theorem map_apply_toReal [Fintype α] [DecidableEq β] (p : PMF α) (f : α → β) (b : β) : + ((p.map f) b).toReal = ∑ a, if b = f a then (p a).toReal else 0 := by + change (p.bind (fun a => PMF.pure (f a)) b).toReal = _ + rw [bind_apply_toReal] + apply Finset.sum_congr rfl + intro a _ + by_cases h : b = f a <;> simp [PMF.pure_apply, h] + +/-- Averaging a score after a deterministic map is averaging its composite with that map. -/ +theorem sum_map_mul [Fintype α] [Fintype β] (p : PMF α) (f : α → β) (score : β → ℝ) : + ∑ b, ((p.map f) b).toReal * score b = ∑ a, (p a).toReal * score (f a) := by + classical + simp only [map_apply_toReal, Finset.sum_mul] + rw [Finset.sum_comm] + simp [ite_mul] + +/-- Averaging a score after a random choice averages its conditional scores. -/ +theorem sum_bind_mul [Fintype α] [Fintype β] (p : PMF α) (kernel : α → PMF β) + (score : β → ℝ) : + ∑ b, (p.bind kernel b).toReal * score b = + ∑ a, (p a).toReal * ∑ b, (kernel a b).toReal * score b := by + simp only [bind_apply_toReal, Finset.sum_mul, Finset.mul_sum, mul_assoc] + exact Finset.sum_comm + +/-- The expectation of an affine score is the same affine function of its expectation. -/ +theorem sum_affine [Fintype α] (p : PMF α) (a b : ℝ) (score : α → ℝ) : + (∑ x, (p x).toReal * (a + b * score x)) = + a + b * ∑ x, (p x).toReal * score x := by + simp only [mul_add, mul_left_comm _ b, Finset.sum_add_distrib, ← Finset.sum_mul, + sum_toReal, one_mul, ← Finset.mul_sum] + +/-- A uniform upper bound on a score also bounds its expectation. -/ +theorem sum_mul_le [Fintype α] (p : PMF α) (score : α → ℝ) (bound : ℝ) + (hscore : ∀ a, score a ≤ bound) : + ∑ a, (p a).toReal * score a ≤ bound := by + calc + _ ≤ ∑ a, (p a).toReal * bound := Finset.sum_le_sum (fun a _ => + mul_le_mul_of_nonneg_left (hscore a) ENNReal.toReal_nonneg) + _ = bound := by rw [← Finset.sum_mul, sum_toReal, one_mul] + /-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)` gives the product `p a * f a b`. -/ theorem bind_pair_apply (p : PMF α) (f : α → PMF β) (a : α) (b : β) : From 0b799231044c19131a29c5567c018592251270ae Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 4 Oct 2026 19:01:53 -0400 Subject: [PATCH 2/5] style(Probability): unsqueeze terminal simps in real-valued PMF lemmas --- Cslib/Probability/PMF.lean | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 58a57c7a2..9bb306d2d 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -90,7 +90,7 @@ theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) := /-- The real-valued probabilities of a finite distribution sum to one. -/ theorem sum_toReal [Fintype α] (p : PMF α) : - ∑ a, (p a).toReal = 1 := by simpa only [tsum_fintype] using tsum_toReal p + ∑ a, (p a).toReal = 1 := by simpa using tsum_toReal p /-- An event has probability at most one. -/ theorem toOuterMeasure_le_one (p : PMF α) (event : Set α) : p.toOuterMeasure event ≤ 1 := by @@ -118,16 +118,13 @@ theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] convert p.tsum_coe using 1 - congr 1 - funext a - by_cases ha : a ∈ event <;> simp [ha] - simpa only [ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _), - ENNReal.toReal_one] using congrArg ENNReal.toReal h + simp + simpa [ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _)] + using congrArg ENNReal.toReal h /-- An event has positive real probability exactly when it contains a possible outcome. -/ theorem toOuterMeasure_toReal_pos_iff (p : PMF α) (event : Set α) : 0 < (p.toOuterMeasure event).toReal ↔ ∃ a ∈ event, a ∈ p.support := by - classical simp [ENNReal.toReal_pos_iff, lt_top_iff_ne_top, toOuterMeasure_ne_top, pos_iff_ne_zero, PMF.toOuterMeasure_apply_eq_zero_iff, Set.disjoint_left, and_comm] @@ -138,7 +135,7 @@ theorem filter_apply_toReal (p : PMF α) (event : Set α) ((p.filter event hevent) a).toReal = if a ∈ event then (p a).toReal / (p.toOuterMeasure event).toReal else 0 := by rw [PMF.filter_apply, ← PMF.toOuterMeasure_apply] - by_cases ha : a ∈ event <;> simp [ha, ENNReal.toReal_mul, div_eq_mul_inv] + by_cases ha : a ∈ event <;> simp [ha, div_eq_mul_inv] /-- Event probability after a finite random choice is the average conditional probability. -/ theorem toOuterMeasure_bind_toReal [Fintype α] (p : PMF α) (kernel : α → PMF β) @@ -147,30 +144,29 @@ theorem toOuterMeasure_bind_toReal [Fintype α] (p : PMF α) (kernel : α → PM ∑ a, (p a).toReal * ((kernel a).toOuterMeasure event).toReal := by rw [PMF.toOuterMeasure_bind_apply, tsum_fintype, ENNReal.toReal_sum (fun a _ => ENNReal.mul_ne_top (PMF.apply_ne_top _ _) (toOuterMeasure_ne_top _ _))] - simp only [ENNReal.toReal_mul] + simp /-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/ theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) : (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by rw [PMF.bind_apply, ENNReal.tsum_toReal_eq (fun a => ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b))] - simp only [ENNReal.toReal_mul] + simp /-- The probability of an outcome after a finite random choice is its weighted average. -/ theorem bind_apply_toReal [Fintype α] (p : PMF α) (kernel : α → PMF β) (b : β) : (p.bind kernel b).toReal = ∑ a, (p a).toReal * (kernel a b).toReal := by - simpa only [tsum_fintype] using bind_apply_toReal_tsum p kernel b + simpa using bind_apply_toReal_tsum p kernel b /-- The mass of a deterministic image is the sum of the masses in its fiber. -/ theorem map_apply_toReal [Fintype α] [DecidableEq β] (p : PMF α) (f : α → β) (b : β) : ((p.map f) b).toReal = ∑ a, if b = f a then (p a).toReal else 0 := by - change (p.bind (fun a => PMF.pure (f a)) b).toReal = _ - rw [bind_apply_toReal] + rw [← PMF.bind_pure_comp, bind_apply_toReal] apply Finset.sum_congr rfl intro a _ - by_cases h : b = f a <;> simp [PMF.pure_apply, h] + by_cases h : b = f a <;> simp [h] /-- Averaging a score after a deterministic map is averaging its composite with that map. -/ theorem sum_map_mul [Fintype α] [Fintype β] (p : PMF α) (f : α → β) (score : β → ℝ) : @@ -178,7 +174,7 @@ theorem sum_map_mul [Fintype α] [Fintype β] (p : PMF α) (f : α → β) (scor classical simp only [map_apply_toReal, Finset.sum_mul] rw [Finset.sum_comm] - simp [ite_mul] + simp /-- Averaging a score after a random choice averages its conditional scores. -/ theorem sum_bind_mul [Fintype α] [Fintype β] (p : PMF α) (kernel : α → PMF β) @@ -192,8 +188,8 @@ theorem sum_bind_mul [Fintype α] [Fintype β] (p : PMF α) (kernel : α → PMF theorem sum_affine [Fintype α] (p : PMF α) (a b : ℝ) (score : α → ℝ) : (∑ x, (p x).toReal * (a + b * score x)) = a + b * ∑ x, (p x).toReal * score x := by - simp only [mul_add, mul_left_comm _ b, Finset.sum_add_distrib, ← Finset.sum_mul, - sum_toReal, one_mul, ← Finset.mul_sum] + simp [mul_add, mul_left_comm _ b, Finset.sum_add_distrib, ← Finset.sum_mul, sum_toReal, + ← Finset.mul_sum] /-- A uniform upper bound on a score also bounds its expectation. -/ theorem sum_mul_le [Fintype α] (p : PMF α) (score : α → ℝ) (bound : ℝ) From e0f27f9b8a975323ba6c43245813ecf4318e0a67 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 4 Oct 2026 19:18:24 -0400 Subject: [PATCH 3/5] style(Probability): rewrite instead of simpa in toOuterMeasure_toReal_add_compl --- Cslib/Probability/PMF.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 9bb306d2d..88798f0dc 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -117,10 +117,9 @@ theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1 := by have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] - convert p.tsum_coe using 1 - simp - simpa [ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _)] - using congrArg ENNReal.toReal h + simp [Set.indicator_self_add_compl_apply] + rw [← ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _), h, + ENNReal.toReal_one] /-- An event has positive real probability exactly when it contains a possible outcome. -/ theorem toOuterMeasure_toReal_pos_iff (p : PMF α) (event : Set α) : From 225dd5e4eaf7afe764d667bd38f444edd1a1ed83 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 5 Oct 2026 15:50:59 -0400 Subject: [PATCH 4/5] refactor(Probability): retain only the PMF prerequisite lemmas --- Cslib/Probability/PMF.lean | 93 -------------------------------------- 1 file changed, 93 deletions(-) diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 88798f0dc..65840c367 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -92,59 +92,6 @@ theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) := theorem sum_toReal [Fintype α] (p : PMF α) : ∑ a, (p a).toReal = 1 := by simpa using tsum_toReal p -/-- An event has probability at most one. -/ -theorem toOuterMeasure_le_one (p : PMF α) (event : Set α) : p.toOuterMeasure event ≤ 1 := by - rw [PMF.toOuterMeasure_apply, ← p.tsum_coe] - exact ENNReal.tsum_le_tsum (fun a => Set.indicator_apply_le (fun _ => le_rfl)) - -/-- The probability of any event is finite. -/ -theorem toOuterMeasure_ne_top (p : PMF α) (event : Set α) : p.toOuterMeasure event ≠ ⊤ := - ne_of_lt ((toOuterMeasure_le_one p event).trans_lt ENNReal.one_lt_top) - -open Classical in -/-- Event probabilities on finite spaces are sums of the masses of their members. -/ -theorem toOuterMeasure_apply_toReal [Fintype α] (p : PMF α) (event : Set α) : - (p.toOuterMeasure event).toReal = ∑ a, if a ∈ event then (p a).toReal else 0 := by - rw [PMF.toOuterMeasure_apply_fintype, ENNReal.toReal_sum] - · apply Finset.sum_congr rfl - intro a _ - by_cases ha : a ∈ event <;> simp [ha] - · intro a _ - by_cases ha : a ∈ event <;> simp [ha, PMF.apply_ne_top] - -/-- An event and its complement have total probability one, in real-valued probability units. -/ -theorem toOuterMeasure_toReal_add_compl (p : PMF α) (event : Set α) : - (p.toOuterMeasure event).toReal + (p.toOuterMeasure eventᶜ).toReal = 1 := by - have h : p.toOuterMeasure event + p.toOuterMeasure eventᶜ = 1 := by - rw [PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply, ← ENNReal.tsum_add] - simp [Set.indicator_self_add_compl_apply] - rw [← ENNReal.toReal_add (toOuterMeasure_ne_top p _) (toOuterMeasure_ne_top p _), h, - ENNReal.toReal_one] - -/-- An event has positive real probability exactly when it contains a possible outcome. -/ -theorem toOuterMeasure_toReal_pos_iff (p : PMF α) (event : Set α) : - 0 < (p.toOuterMeasure event).toReal ↔ ∃ a ∈ event, a ∈ p.support := by - simp [ENNReal.toReal_pos_iff, lt_top_iff_ne_top, toOuterMeasure_ne_top, pos_iff_ne_zero, - PMF.toOuterMeasure_apply_eq_zero_iff, Set.disjoint_left, and_comm] - -open Classical in -/-- Conditioning keeps the event's masses and divides them by its probability. -/ -theorem filter_apply_toReal (p : PMF α) (event : Set α) - (hevent : ∃ a ∈ event, a ∈ p.support) (a : α) : - ((p.filter event hevent) a).toReal = - if a ∈ event then (p a).toReal / (p.toOuterMeasure event).toReal else 0 := by - rw [PMF.filter_apply, ← PMF.toOuterMeasure_apply] - by_cases ha : a ∈ event <;> simp [ha, div_eq_mul_inv] - -/-- Event probability after a finite random choice is the average conditional probability. -/ -theorem toOuterMeasure_bind_toReal [Fintype α] (p : PMF α) (kernel : α → PMF β) - (event : Set β) : - ((p.bind kernel).toOuterMeasure event).toReal = - ∑ a, (p a).toReal * ((kernel a).toOuterMeasure event).toReal := by - rw [PMF.toOuterMeasure_bind_apply, tsum_fintype, ENNReal.toReal_sum - (fun a _ => ENNReal.mul_ne_top (PMF.apply_ne_top _ _) (toOuterMeasure_ne_top _ _))] - simp - /-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/ theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) : (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by @@ -159,46 +106,6 @@ theorem bind_apply_toReal [Fintype α] (p : PMF α) ∑ a, (p a).toReal * (kernel a b).toReal := by simpa using bind_apply_toReal_tsum p kernel b -/-- The mass of a deterministic image is the sum of the masses in its fiber. -/ -theorem map_apply_toReal [Fintype α] [DecidableEq β] (p : PMF α) (f : α → β) (b : β) : - ((p.map f) b).toReal = ∑ a, if b = f a then (p a).toReal else 0 := by - rw [← PMF.bind_pure_comp, bind_apply_toReal] - apply Finset.sum_congr rfl - intro a _ - by_cases h : b = f a <;> simp [h] - -/-- Averaging a score after a deterministic map is averaging its composite with that map. -/ -theorem sum_map_mul [Fintype α] [Fintype β] (p : PMF α) (f : α → β) (score : β → ℝ) : - ∑ b, ((p.map f) b).toReal * score b = ∑ a, (p a).toReal * score (f a) := by - classical - simp only [map_apply_toReal, Finset.sum_mul] - rw [Finset.sum_comm] - simp - -/-- Averaging a score after a random choice averages its conditional scores. -/ -theorem sum_bind_mul [Fintype α] [Fintype β] (p : PMF α) (kernel : α → PMF β) - (score : β → ℝ) : - ∑ b, (p.bind kernel b).toReal * score b = - ∑ a, (p a).toReal * ∑ b, (kernel a b).toReal * score b := by - simp only [bind_apply_toReal, Finset.sum_mul, Finset.mul_sum, mul_assoc] - exact Finset.sum_comm - -/-- The expectation of an affine score is the same affine function of its expectation. -/ -theorem sum_affine [Fintype α] (p : PMF α) (a b : ℝ) (score : α → ℝ) : - (∑ x, (p x).toReal * (a + b * score x)) = - a + b * ∑ x, (p x).toReal * score x := by - simp [mul_add, mul_left_comm _ b, Finset.sum_add_distrib, ← Finset.sum_mul, sum_toReal, - ← Finset.mul_sum] - -/-- A uniform upper bound on a score also bounds its expectation. -/ -theorem sum_mul_le [Fintype α] (p : PMF α) (score : α → ℝ) (bound : ℝ) - (hscore : ∀ a, score a ≤ bound) : - ∑ a, (p a).toReal * score a ≤ bound := by - calc - _ ≤ ∑ a, (p a).toReal * bound := Finset.sum_le_sum (fun a _ => - mul_le_mul_of_nonneg_left (hscore a) ENNReal.toReal_nonneg) - _ = bound := by rw [← Finset.sum_mul, sum_toReal, one_mul] - /-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)` gives the product `p a * f a b`. -/ theorem bind_pair_apply (p : PMF α) (f : α → PMF β) (a : α) (b : β) : From 630f6418380819c5f5d9eda0b467a65ede99b2b7 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 7 Oct 2026 02:00:06 -0400 Subject: [PATCH 5/5] fix(Probability): avoid PMF insertion conflict with main --- Cslib/Probability/PMF.lean | 52 +++++++++++++++++++------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 65840c367..e34927505 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -80,32 +80,6 @@ theorem uniformOfFintype_apply [Fintype α] [Nonempty α] (a : α) : uniformOfFintype α a = (Fintype.card α : ℝ≥0∞)⁻¹ := by simp [uniformOfFintype] -/-- Real-valued probability masses are summable, even on an infinite ambient type. -/ -theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) := - ENNReal.summable_toReal p.tsum_coe_ne_top - -/-- The real-valued masses of any discrete distribution sum to one. -/ -@[simp] theorem tsum_toReal (p : PMF α) : ∑' a, (p a).toReal = 1 := by - rw [← ENNReal.tsum_toReal_eq p.apply_ne_top, p.tsum_coe, ENNReal.toReal_one] - -/-- The real-valued probabilities of a finite distribution sum to one. -/ -theorem sum_toReal [Fintype α] (p : PMF α) : - ∑ a, (p a).toReal = 1 := by simpa using tsum_toReal p - -/-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/ -theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) : - (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by - rw [PMF.bind_apply, ENNReal.tsum_toReal_eq (fun a => - ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b))] - simp - -/-- The probability of an outcome after a finite random choice is its weighted average. -/ -theorem bind_apply_toReal [Fintype α] (p : PMF α) - (kernel : α → PMF β) (b : β) : - (p.bind kernel b).toReal = - ∑ a, (p a).toReal * (kernel a b).toReal := by - simpa using bind_apply_toReal_tsum p kernel b - /-- Evaluating the "pairing" bind `(do let a ← p; return (a, ← f a))` at `(a, b)` gives the product `p a * f a b`. -/ theorem bind_pair_apply (p : PMF α) (f : α → PMF β) (a : α) (b : β) : @@ -162,4 +136,30 @@ theorem posteriorDist_eq_prior_of_outputIndist (p : PMF α) (f : α → PMF β) exact ENNReal.mul_div_cancel_right ((PMF.mem_support_iff _ _).mp (hbind ▸ hb)) (PMF.apply_ne_top _ _) +/-- Real-valued probability masses are summable, even on an infinite ambient type. -/ +theorem summable_toReal (p : PMF α) : Summable (fun a => (p a).toReal) := + ENNReal.summable_toReal p.tsum_coe_ne_top + +/-- The real-valued masses of any discrete distribution sum to one. -/ +@[simp] theorem tsum_toReal (p : PMF α) : ∑' a, (p a).toReal = 1 := by + rw [← ENNReal.tsum_toReal_eq p.apply_ne_top, p.tsum_coe, ENNReal.toReal_one] + +/-- The real-valued probabilities of a finite distribution sum to one. -/ +theorem sum_toReal [Fintype α] (p : PMF α) : + ∑ a, (p a).toReal = 1 := by simpa using tsum_toReal p + +/-- Randomized postprocessing averages the outcome probabilities over any discrete input. -/ +theorem bind_apply_toReal_tsum (p : PMF α) (kernel : α → PMF β) (b : β) : + (p.bind kernel b).toReal = ∑' a, (p a).toReal * (kernel a b).toReal := by + rw [PMF.bind_apply, ENNReal.tsum_toReal_eq (fun a => + ENNReal.mul_ne_top (p.apply_ne_top a) ((kernel a).apply_ne_top b))] + simp + +/-- The probability of an outcome after a finite random choice is its weighted average. -/ +theorem bind_apply_toReal [Fintype α] (p : PMF α) + (kernel : α → PMF β) (b : β) : + (p.bind kernel b).toReal = + ∑ a, (p a).toReal * (kernel a b).toReal := by + simpa using bind_apply_toReal_tsum p kernel b + end Cslib.Probability.PMF