diff --git a/Complexity.lean b/Complexity.lean index 4a3ea89215..5a7def5a97 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2805,6 +2805,7 @@ public import Complexity.Languages.Probabilistic.BitString public import Complexity.Languages.Probabilistic.BoundedUniform public import Complexity.Languages.Probabilistic.CenteredBinomial public import Complexity.Languages.Probabilistic.Concentration +public import Complexity.Languages.Probabilistic.Event public import Complexity.Languages.Probabilistic.Expect public import Complexity.Languages.Probabilistic.Forking public import Complexity.Languages.Probabilistic.Iteration diff --git a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean index ff044ccf5c..d0be8fc275 100644 --- a/Complexity/Algorithms/WordRAM/Karger/FastCut.lean +++ b/Complexity/Algorithms/WordRAM/Karger/FastCut.lean @@ -69,13 +69,11 @@ minimum-cut-value part of Theorem 4.4; paraphrase) on the randomized word RAM. * `Cslib.Algorithms.WordRAM.Karger.fastCutScratch_le`: total root-to-leaf stack workspace bound `fastCutScratch n ≤ 26 * (n * n)` for `n ≥ 2` (`[KargerStein1996]`, Section 4, Lemma 4.2; paraphrase). -* `Cslib.Algorithms.WordRAM.Karger.two_branch_hit_prob_ge`, - `Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq`, - `Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le`: elementary `ENNReal` probability - recurrence `1 - (1 - 1 / s) ^ 2 ≥ 2 / (s + 1)` giving `≥ 1 / (Nat.log 2 n + 15)` single-tree - success (`[KargerStein1996]`, Section 4, Lemma 4.3; paraphrase) and `≤ 1 / (2 * n)` amplified - failure (the minimum-cut-value part of `[KargerStein1996]`, Section 4, Theorem 4.4; paraphrase) - without `Real.log` or `Real.exp`. +* `Cslib.Algorithms.WordRAM.Karger.root_hit_prob_eq`: normalize the root-depth success bound to + `1 / (Nat.log 2 n + 15)` (`[KargerStein1996]`, Section 4, Lemma 4.3; paraphrase). +* `Cslib.Algorithms.WordRAM.Karger.fastCutHighProb_failure_le`: amplified failure bound + `≤ 1 / (2 * n)` (the minimum-cut-value part of `[KargerStein1996]`, Section 4, Theorem 4.4; + paraphrase), without `Real.log` or `Real.exp`. ## References @@ -589,92 +587,6 @@ private theorem one_sub_inv_nat {s : ℕ} (hs : 1 ≤ s) : exact_mod_cast Nat.sub_add_cancel hs rw [hsub, ← div_eq_mul_inv, ENNReal.div_self hs0 hst] -/-- Elementary recurrence `2 / (s + 1) ≤ 1 - (1 - 1 / s) ^ 2` in `ℝ≥0∞` for `1 ≤ s`, derived from -`(2 * s - 1) * (s + 1) = 2 * s ^ 2 + s - 1 ≥ 2 * s ^ 2`. -/ -theorem one_sub_sq_one_sub_inv_ge {s : ℕ} (hs : 1 ≤ s) : - (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by - rw [one_sub_inv_nat hs] - have hs0 : (s : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : s ≠ 0) - have hst : (s : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top s - have hs20 : ((s * s : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (Nat.mul_pos hs hs).ne' - have hs2t : ((s * s : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ - have hsp10 : ((s + 1 : ℕ) : ℝ≥0∞) ≠ 0 := by positivity - have hsp1t : ((s + 1 : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ - have hsq_eq : (((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 = - (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by - simp only [sq, div_eq_mul_inv, Nat.cast_mul, ENNReal.mul_inv (Or.inl hs0) (Or.inl hst)] - ring - rw [hsq_eq] - have hsub_eq : (1 : ℝ≥0∞) - (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) = - ((2 * s - 1 : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by - refine ENNReal.sub_eq_of_eq_add - (ENNReal.div_ne_top (ENNReal.natCast_ne_top _) hs20) ?_ - rw [div_eq_mul_inv, div_eq_mul_inv, ← add_mul] - have hsum : (2 * s - 1) + (s - 1) * (s - 1) = s * s := by - obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩ - have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega - have h2 : d + 1 - 1 = d := by omega - rw [h1, h2] - ring - have hcast : ((2 * s - 1 : ℕ) : ℝ≥0∞) + (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) = - ((s * s : ℕ) : ℝ≥0∞) := by exact_mod_cast hsum - rw [hcast, ← div_eq_mul_inv, ENNReal.div_self hs20 hs2t] - rw [hsub_eq] - rw [ENNReal.div_le_iff_le_mul (Or.inl hsp10) (Or.inl hsp1t)] - rw [← ENNReal.mul_div_right_comm] - rw [ENNReal.le_div_iff_mul_le (Or.inl hs20) (Or.inl hs2t)] - have hnat : 2 * (s * s) ≤ (2 * s - 1) * (s + 1) := by - obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩ - have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega - rw [h1] - nlinarith - exact_mod_cast hnat - -/-- Sequential two-branch success probability recurrence on `ProbComp`: if Branch 1 hits `hit₁` -with probability `≥ 1 / s`, any outcome in `hit₁` guarantees `f a b ∈ hit` on every supported `b`, -and conditioned on any outcome outside `hit₁` Branch 2 achieves `f a b ∈ hit` with probability -`≥ 1 / s`, then the combined computation hits `hit` with probability `≥ 2 / (s + 1)`. -/ -theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α → ProbComp β) - (f : α → β → γ) (hit₁ : Set α) (hit : Set γ) {s : ℕ} (hs : 1 ≤ s) - (hb₁ : (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ m₁.eval.toOuterMeasure hit₁) - (hprop₁ : ∀ a ∈ m₁.support, a ∈ hit₁ → ∀ b ∈ (m₂ a).support, f a b ∈ hit) - (hb₂ : ∀ a ∈ m₁.support, a ∉ hit₁ → - (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ ((m₂ a).eval.map (f a)).toOuterMeasure hit) : - (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ - (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval.toOuterMeasure hit := by - let p := (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval - have hp_eq : p = m₁.eval.bind (fun a => (m₂ a).eval.map (f a)) := by - dsimp only [p] - rw [ProbComp.eval_bind] - refine congrArg (m₁.eval.bind ·) (funext fun a => ?_) - rw [bind_pure_comp, ProbComp.eval_map] - have hcompl_le : p.toOuterMeasure hitᶜ ≤ (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by - rw [hp_eq, sq] - refine toOuterMeasure_bind_le_mul_ennreal m₁.eval (fun a => (m₂ a).eval.map (f a)) - hit₁ᶜ hitᶜ (toOuterMeasure_compl_le_one_sub m₁.eval hit₁ hb₁) ?_ ?_ - · intro a ha_eval ha_miss - have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval - exact toOuterMeasure_compl_le_one_sub _ hit (hb₂ a ha ha_miss) - · intro a ha_eval ha_not_miss - have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval - have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss - rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] - refine tsum_eq_zero_iff.mpr fun b => ?_ - by_cases hb_eval : b ∈ (m₂ a).eval.support - · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval - have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb - have hnot : b ∉ (f a ⁻¹' hitᶜ) := fun hc => hc hmem - exact Set.indicator_of_notMem hnot _ - · have hp0 : (m₂ a).eval b = 0 := by simpa only [PMF.mem_support_iff, not_not] using hb_eval - simp [hp0] - have hsum := toOuterMeasure_add_compl_ennreal p hit - have hhit_ge : 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 ≤ p.toOuterMeasure hit := by - refine tsub_le_iff_right.mpr ?_ - calc - (1 : ℝ≥0∞) = p.toOuterMeasure hit + p.toOuterMeasure hitᶜ := hsum.symm - _ ≤ p.toOuterMeasure hit + (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by gcongr - exact (one_sub_sq_one_sub_inv_ge hs).trans hhit_ge - /-- At the root depth budget `d = 2 * Nat.log 2 n`, `2 / (d + 30) = 1 / (Nat.log 2 n + 15)`. -/ theorem root_hit_prob_eq (n : ℕ) : (2 : ℝ≥0∞) / ((2 * Nat.log 2 n + 30 : ℕ) : ℝ≥0∞) = diff --git a/Complexity/Algorithms/WordRAM/KargerStein.lean b/Complexity/Algorithms/WordRAM/KargerStein.lean index d9304e7812..5f1acba8ad 100644 --- a/Complexity/Algorithms/WordRAM/KargerStein.lean +++ b/Complexity/Algorithms/WordRAM/KargerStein.lean @@ -14,6 +14,7 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut public import Complexity.Computability.WordRAM.Copy public import Complexity.Computability.WordRAM.Randomized.LoopSegment public import Complexity.Computability.WordRAM.Time +import Complexity.Languages.Probabilistic.Event /-! # Karger–Stein's recursive `FastCut` algorithm on the word RAM @@ -2725,7 +2726,7 @@ theorem fastCutNode_spec {n w : ℕ} {W₀ : Fin n → Fin n → ℕ} dsimp only [t] at ht₁ ht₂ omega · intro B hmin_pos hB_nt hB_min - have hrec := two_branch_hit_prob_ge m_b1 (fun z₁ => m₂_fn z₁.1) + have hrec := ProbComp.two_branch_hit_prob_ge m_b1 (fun z₁ => m₂_fn z₁.1) (fun z₁ z₂ => (z₂.1, z₁.2 + z₂.2)) {z₁ | z₁.1.regs retVal = minCut W₀} {z | z.1.regs retVal = minCut W₀} diff --git a/Complexity/Languages/Probabilistic/Event.lean b/Complexity/Languages/Probabilistic/Event.lean new file mode 100644 index 0000000000..8c442f1f58 --- /dev/null +++ b/Complexity/Languages/Probabilistic/Event.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2026 Renfei Zhou, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Renfei Zhou, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.Semantics +import Complexity.Probability.PMF.Event + +/-! +# Sequential success bounds for probabilistic programs + +A first program can establish success, and a second program can recover when the first fails. +If each branch succeeds with probability at least `1 / s` on the inputs that need it, and later +execution retains every first-branch success, the sequence succeeds with probability at least +`2 / (s + 1)`. The second program may depend on the first result. Hypotheses apply only to +possible outcomes, and no independence or finite output-type hypothesis is needed. + +These are bounds on the distributions denoted by terminating `ProbComp` programs. Runtime and +oracle-query costs require separate certificates. + +## Main results + +* `Cslib.ProbComp.two_branch_hit_prob_ge`: retained first-branch success and conditional recovery + give the two-branch success bound. + +## References + +The generic success rule is from Renfei Zhou's Karger–Stein development. +-/ + +@[expose] public section + +namespace Cslib.ProbComp + +open scoped ENNReal +open Cslib.Probability.PMF + +/-- Elementary recurrence `2 / (s + 1) ≤ 1 - (1 - 1 / s) ^ 2` in `ℝ≥0∞` for `1 ≤ s`, derived from +`(2 * s - 1) * (s + 1) = 2 * s ^ 2 + s - 1 ≥ 2 * s ^ 2`. -/ +private theorem one_sub_sq_one_sub_inv_ge {s : ℕ} (hs : 1 ≤ s) : + (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by + have hs0 : (s : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : s ≠ 0) + have hst : (s : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top s + have hsub : (1 : ℝ≥0∞) - 1 / (s : ℝ≥0∞) = + ((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞) := by + rw [ENNReal.natCast_sub, Nat.cast_one, ENNReal.sub_div (fun _ _ => hs0), + ENNReal.div_self hs0 hst] + rw [hsub] + have hs20 : ((s * s : ℕ) : ℝ≥0∞) ≠ 0 := by exact_mod_cast (Nat.mul_pos hs hs).ne' + have hs2t : ((s * s : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ + have hsp10 : ((s + 1 : ℕ) : ℝ≥0∞) ≠ 0 := by positivity + have hsp1t : ((s + 1 : ℕ) : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ + have hsq_eq : (((s - 1 : ℕ) : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 = + (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by + simp only [sq, div_eq_mul_inv, Nat.cast_mul, ENNReal.mul_inv (Or.inl hs0) (Or.inl hst)] + ring + rw [hsq_eq] + have hsub_eq : (1 : ℝ≥0∞) - (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) = + ((2 * s - 1 : ℕ) : ℝ≥0∞) / ((s * s : ℕ) : ℝ≥0∞) := by + refine ENNReal.sub_eq_of_eq_add + (ENNReal.div_ne_top (ENNReal.natCast_ne_top _) hs20) ?_ + rw [div_eq_mul_inv, div_eq_mul_inv, ← add_mul] + have hsum : (2 * s - 1) + (s - 1) * (s - 1) = s * s := by + obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩ + have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega + have h2 : d + 1 - 1 = d := by omega + rw [h1, h2] + ring + have hcast : ((2 * s - 1 : ℕ) : ℝ≥0∞) + (((s - 1) * (s - 1) : ℕ) : ℝ≥0∞) = + ((s * s : ℕ) : ℝ≥0∞) := by exact_mod_cast hsum + rw [hcast, ← div_eq_mul_inv, ENNReal.div_self hs20 hs2t] + rw [hsub_eq] + rw [ENNReal.div_le_iff_le_mul (Or.inl hsp10) (Or.inl hsp1t)] + rw [← ENNReal.mul_div_right_comm] + rw [ENNReal.le_div_iff_mul_le (Or.inl hs20) (Or.inl hs2t)] + have hnat : 2 * (s * s) ≤ (2 * s - 1) * (s + 1) := by + obtain ⟨d, rfl⟩ : ∃ d, s = d + 1 := ⟨s - 1, by omega⟩ + have h1 : 2 * (d + 1) - 1 = 2 * d + 1 := by omega + rw [h1] + nlinarith + exact_mod_cast hnat + +/-- Sequential two-branch success probability recurrence on `ProbComp`: if Branch 1 hits `hit₁` +with probability `≥ 1 / s`, any outcome in `hit₁` guarantees `f a b ∈ hit` on every supported `b`, +and conditioned on any outcome outside `hit₁` Branch 2 achieves `f a b ∈ hit` with probability +`≥ 1 / s`, then the combined computation hits `hit` with probability `≥ 2 / (s + 1)`. -/ +theorem two_branch_hit_prob_ge {α β γ : Type} (m₁ : ProbComp α) (m₂ : α → ProbComp β) + (f : α → β → γ) (hit₁ : Set α) (hit : Set γ) {s : ℕ} (hs : 1 ≤ s) + (hb₁ : (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ m₁.eval.toOuterMeasure hit₁) + (hprop₁ : ∀ a ∈ m₁.support, a ∈ hit₁ → ∀ b ∈ (m₂ a).support, f a b ∈ hit) + (hb₂ : ∀ a ∈ m₁.support, a ∉ hit₁ → + (1 : ℝ≥0∞) / (s : ℝ≥0∞) ≤ ((m₂ a).eval.map (f a)).toOuterMeasure hit) : + (2 : ℝ≥0∞) / ((s + 1 : ℕ) : ℝ≥0∞) ≤ + (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval.toOuterMeasure hit := by + let p := (do let a ← m₁; let b ← m₂ a; pure (f a b)).eval + have hp_eq : p = m₁.eval.bind (fun a => (m₂ a).eval.map (f a)) := by + dsimp only [p] + rw [ProbComp.eval_bind] + refine congrArg (m₁.eval.bind ·) (funext fun a => ?_) + rw [bind_pure_comp, ProbComp.eval_map] + have hcompl_le : p.toOuterMeasure hitᶜ ≤ (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by + rw [hp_eq, sq] + refine toOuterMeasure_bind_le_mul_ennreal m₁.eval (fun a => (m₂ a).eval.map (f a)) + hit₁ᶜ hitᶜ (toOuterMeasure_compl_le_one_sub m₁.eval hit₁ hb₁) ?_ ?_ + · intro a ha_eval ha_miss + have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval + exact toOuterMeasure_compl_le_one_sub _ hit (hb₂ a ha ha_miss) + · intro a ha_eval ha_not_miss + have ha : a ∈ m₁.support := (ProbComp.support_eval m₁) ▸ ha_eval + have ha_hit : a ∈ hit₁ := not_not.mp ha_not_miss + rw [PMF.toOuterMeasure_map_apply, PMF.toOuterMeasure_apply] + refine tsum_eq_zero_iff.mpr fun b => ?_ + by_cases hb_eval : b ∈ (m₂ a).eval.support + · have hb : b ∈ (m₂ a).support := (ProbComp.support_eval (m₂ a)) ▸ hb_eval + have hmem : f a b ∈ hit := hprop₁ a ha ha_hit b hb + have hnot : b ∉ (f a ⁻¹' hitᶜ) := fun hc => hc hmem + exact Set.indicator_of_notMem hnot _ + · have hp0 : (m₂ a).eval b = 0 := by simpa only [PMF.mem_support_iff, not_not] using hb_eval + simp [hp0] + have hsum := toOuterMeasure_add_compl_ennreal p hit + have hhit_ge : 1 - (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 ≤ p.toOuterMeasure hit := by + refine tsub_le_iff_right.mpr ?_ + calc + (1 : ℝ≥0∞) = p.toOuterMeasure hit + p.toOuterMeasure hitᶜ := hsum.symm + _ ≤ p.toOuterMeasure hit + (1 - (1 : ℝ≥0∞) / (s : ℝ≥0∞)) ^ 2 := by gcongr + exact (one_sub_sq_one_sub_inv_ge hs).trans hhit_ge + +end Cslib.ProbComp diff --git a/ComplexityTests/ProbCompEvent.lean b/ComplexityTests/ProbCompEvent.lean new file mode 100644 index 0000000000..f55d3a476d --- /dev/null +++ b/ComplexityTests/ProbCompEvent.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Languages.Probabilistic.Event + +/-! Shared probabilistic-program success bounds, without a graph-algorithm import. -/ + +namespace ComplexityTests.ProbCompEvent + +open Cslib +open scoped ENNReal + +private theorem coin_hit : + (1 : ℝ≥0∞) / 2 ≤ (ProbComp.uniform Bool).eval.toOuterMeasure {true} := by + rw [ProbComp.eval_uniform, PMF.toOuterMeasure_apply_singleton, + Probability.PMF.uniformOfFintype_apply] + norm_num + +-- The first success skips the second draw; a fresh coin recovers after failure. The +-- continuation depends on the first result, and the shared bound gives at least `2 / 3`. +example : (2 : ℝ≥0∞) / 3 ≤ (do + let a ← ProbComp.uniform Bool + let b ← (if a then pure false else ProbComp.uniform Bool) + pure (a || b)).eval.toOuterMeasure {true} := by + refine ProbComp.two_branch_hit_prob_ge (ProbComp.uniform Bool) + (fun a => if a then pure false else ProbComp.uniform Bool) (fun a b => a || b) + {true} {true} + (s := 2) (by decide) coin_hit ?_ ?_ + · intro a _ ha b _ + change a = true at ha + subst a + simp + · intro a _ ha + have hfalse : a = false := by cases a <;> simp_all + subst a + change (1 : ℝ≥0∞) / 2 ≤ ((ProbComp.uniform Bool).eval.map id).toOuterMeasure {true} + rw [PMF.map_id] + exact coin_hit + +-- At `s = 1`, a certain first success is retained through any later program. The later +-- program need not succeed when given the unsupported first result `false`. +example (later : Bool → ProbComp Bool) : + (1 : ℝ≥0∞) ≤ (do + let a ← (pure true : ProbComp Bool) + let b ← later a + pure (a || b)).eval.toOuterMeasure {true} := by + have h := ProbComp.two_branch_hit_prob_ge (pure true) later (fun a b => a || b) + {true} {true} (s := 1) (by decide) (by simp) (by + intro a _ ha b _ + change a = true at ha + subst a + simp) (by + intro a ha hmiss + have ha' : a = true := OracleComp.eq_of_mem_supportWith_pure ha + exact False.elim (hmiss ha')) + have htwo : (2 : ℝ≥0∞) / 2 = 1 := ENNReal.div_self (by norm_num) (by norm_num) + simpa only [show ((1 + 1 : ℕ) : ℝ≥0∞) = 2 by norm_num, htwo] using h + +end ComplexityTests.ProbCompEvent diff --git a/ROADMAP.md b/ROADMAP.md index 9dbf5b5c6a..e62d285de3 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -757,15 +757,13 @@ reuse is demonstrated. - **One sensitivity API.** Define the sensitivity measures over any `Fintype` in CSLib and drop the separate measures of the sensitivity-separation development. -- **Weighted multigraph cuts and two-branch probability recurrence** ([#1336]): extract +- **Weighted multigraph cuts** ([#1336]): extract `IsMultigraph` (renamed e.g. `IsSymmLoopless` or phrased via `Matrix.IsSymm` with zero diagonal), `IsNonTrivialCut`, `cutWeight`, `minCut`, `rowDeg`, `totalDoubledWeight`, `flattenMatrix`, and `IsContractionOf` from `Complexity/Algorithms/WordRAM/Karger/Graph.lean` (shared by `KargerMinCut` and `KargerStein`) into `Complexity/Foundations/Combinatorics/WeightedCut.lean` with a bridge lemma relating `cutWeight W C` - to `(Cslib.Multigraph.edgeCut ends C).card`. Extract `two_branch_hit_prob_ge` from - `Karger/FastCut.lean` into a shared probabilistic-program module; its `ProbComp` evaluation and - support dependencies should stay above the `PMF` event layer. + to `(Cslib.Multigraph.edgeCut ends C).card`. - **CNF evaluation certificates:** `fun_prop` certificates for evaluating literals, clauses and formulas under a polynomial-time assignment, so clients stop passing `CNF.eval`, `Clause.eval` and `Literal.eval` to `fun_prop` as unfolding hints.