feat(probability): generalize shared heavy-count rarity bounds

Complexity/Foundations/Probability/HeavyCount.lean

@@ -17,9 +17,11 @@ import Mathlib.Tactic.Ring
 /-!
 # Conditional rarity of retained heavy entries
 
-A row with first signal `d` has bounded mass `a * ∑ w, d w ≤ M`. At a floor `ρ > 0`,
-there are at most `4 * M / (a * ρ)` entries above `ρ / 4`. Suppose that, on a finite slice
-of draws, every endpoint other than one specified endpoint is retained on at most a
+A row on a finite endpoint set `S` has first signal `d` and bounded mass
+`a * ∑ w ∈ S, d w ≤ M`. At a floor `ρ > 0`, its heavy-set cardinality satisfies
+`#{w ∈ S | ρ / 4 < d w} * a * ρ ≤ 4 * M`, including at zero scale `a = 0`.
+Suppose that, on a finite slice of draws, every heavy endpoint other than one specified
+endpoint is retained on at most a
 `c * a` fraction of the draws. The specified endpoint can contribute one retained entry.
 Markov's inequality then bounds the fraction of draws retaining at least `n / 2` heavy
 entries by `2 * (1 + 4 * c * M) / (n * ρ)` when `ρ ≤ 1`.
@@ -39,6 +41,10 @@ integrated compression bound are separate steps.
 * `Cslib.Probability.card_filter_heavy_mul_le`: the deterministic heavy-set mass bound.
 * `Cslib.Probability.card_filter_heavyCountEvent_mul_le`: rarity without division.
 * `Cslib.Probability.card_filter_heavyCountEvent_le`: the explicit conditional rarity factor.
+* `Cslib.Probability.card_filter_heavyCountEvent_div_card_le`: the conditional frequency bound,
+  including empty slices.
+* `Cslib.Probability.card_filter_heavyCountEvent_product_div_card_le`: an independent start
+  slice preserves the frequency bound.
 
 ## References
 
@@ -54,62 +60,64 @@ open scoped BigOperators
 
 namespace Cslib.Probability
 
-variable {Ω V : Type*} [Fintype V]
+variable {Ω V : Type*}
 
 open Classical in
 /-- A true heavy count at floor `ρ`: at least half the capacity `n` consists of retained
-endpoints whose deterministic first signal exceeds `ρ / 4`. -/
-@[expose] def heavyCountEvent (Y : Ω → V → Prop) (d : V → ℝ) (ρ : ℝ) (n : ℕ)
+endpoints in `S` whose deterministic first signal exceeds `ρ / 4`. -/
+@[expose] def heavyCountEvent (Y : Ω → V → Prop) (S : Finset V) (d : V → ℝ) (ρ : ℝ) (n : ℕ)
     (σ : Ω) : Prop :=
-  n ≤ 2 * #{w | Y σ w ∧ ρ / 4 < d w}
+  n ≤ 2 * #{w ∈ S | Y σ w ∧ ρ / 4 < d w}
 
 /-- The deterministic mass bounds the number of entries above a quarter of the floor.
 The multiplied form remains valid at zero scale and for every floor. -/
-theorem card_filter_heavy_mul_le {a ρ M : ℝ} {d : V → ℝ} (ha : 0 ≤ a)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M) :
-    (#{w | ρ / 4 < d w} : ℝ) * (a * ρ) ≤ 4 * M := by
+theorem card_filter_heavy_mul_le (S : Finset V) {a ρ M : ℝ} {d : V → ℝ} (ha : 0 ≤ a)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M) :
+    (#{w ∈ S | ρ / 4 < d w} : ℝ) * (a * ρ) ≤ 4 * M := by
   classical
-  have hcount : (#{w | ρ / 4 < d w} : ℝ) * (ρ / 4) ≤ ∑ w, d w :=
-    card_filter_mul_le_sum univ _ d (fun w _ => hd w) fun _ _ hw => hw.le
+  have hcount : (#{w ∈ S | ρ / 4 < d w} : ℝ) * (ρ / 4) ≤ ∑ w ∈ S, d w :=
+    card_filter_mul_le_sum S _ d hd fun _ _ hw => hw.le
   have h := (mul_le_mul_of_nonneg_left hcount ha).trans hmass
   linarith
 
 open Classical in
 /-- Conditional rarity of a true heavy count, without division. The endpoint `y` may be
-forced by the conditioning slice, while all other endpoints satisfy its pair-count bound.
+forced by the conditioning slice, while only the other heavy endpoints need its pair-count bound.
 The slice and the capacity may be empty or zero. -/
-theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V)
-    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hc : 0 ≤ c)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M)
-    (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) (n : ℕ) :
-    (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ ≤
+theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) (n : ℕ) :
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) * n * ρ ≤
       #T * (2 * (ρ + 4 * c * M)) := by
   classical
-  let D : Finset V := {w | ρ / 4 < d w}
+  let D : Finset V := {w ∈ S | ρ / 4 < d w}
   have hfilter (σ : Ω) : ({w ∈ D | Y σ w} : Finset V) =
-      ({w | Y σ w ∧ ρ / 4 < d w} : Finset V) := by
+      ({w ∈ S | Y σ w ∧ ρ / 4 < d w} : Finset V) := by
     ext w
-    simp [D, and_comm]
+    simp [D, and_left_comm, and_comm]
   have hevent (σ : Ω) : (n + 1) / 2 ≤ #{w ∈ D | Y σ w} ↔
-      heavyCountEvent Y d ρ n σ := by
+      heavyCountEvent Y S d ρ n σ := by
     rw [hfilter]
     unfold heavyCountEvent
     omega
-  have hcount := card_filter_le_card_filter_mul_le Y T D y (mul_nonneg hc ha.le)
-    (fun w _ hw => hpair w hw) ((n + 1) / 2)
+  have hcount := card_filter_le_card_filter_mul_le Y T D y (mul_nonneg hc ha)
+    (fun w hw hwy => hpair w (mem_filter.mp hw).1 (mem_filter.mp hw).2 hwy) ((n + 1) / 2)
   simp only [hevent] at hcount
   have hn : (n : ℝ) ≤ 2 * (((n + 1) / 2 : ℕ) : ℝ) := by
     exact_mod_cast (show n ≤ 2 * ((n + 1) / 2) by omega)
   have hmassD : (#D : ℝ) * (a * ρ) ≤ 4 * M :=
-    card_filter_heavy_mul_le ha.le hd hmass
+    card_filter_heavy_mul_le S ha hd hmass
   have hmassc : c * a * #D * ρ ≤ 4 * c * M := by
     have h := mul_le_mul_of_nonneg_left hmassD hc
     nlinarith
   calc
-    _ ≤ (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) *
+    _ ≤ (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) *
         (2 * (((n + 1) / 2 : ℕ) : ℝ)) * ρ :=
       mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hn (by positivity)) hρ.le
-    _ = 2 * ((#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) *
+    _ = 2 * ((#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) *
         (((n + 1) / 2 : ℕ) : ℝ)) * ρ := by ring
     _ ≤ 2 * (#T * (1 + c * a * #D)) * ρ :=
       mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hcount (by norm_num)) hρ.le
@@ -121,23 +129,67 @@ theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset 
 open Classical in
 /-- The conditional rarity factor `2 * (1 + 4 * c * M) / (n * ρ)` for a positive capacity
 and a floor in `(0, 1]`. Empty slices require no special convention. -/
-theorem card_filter_heavyCountEvent_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V)
-    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
-    (hc : 0 ≤ c) (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M)
-    (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T)
+theorem card_filter_heavyCountEvent_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    (hc : 0 ≤ c) (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T)
     {n : ℕ} (hn : 0 < n) :
-    (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) ≤
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) ≤
       (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) * #T := by
   classical
-  have h := card_filter_heavyCountEvent_mul_le Y T y ha hρ hc hd hmass hpair n
+  have h := card_filter_heavyCountEvent_mul_le Y T S y ha hρ hc hd hmass hpair n
   have hn' : (0 : ℝ) < n := by exact_mod_cast hn
   rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hn' hρ)]
   calc
-    _ = (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ := by ring
+    _ = (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) * n * ρ := by ring
     _ ≤ #T * (2 * (ρ + 4 * c * M)) := h
     _ ≤ #T * (2 * (1 + 4 * c * M)) :=
       mul_le_mul_of_nonneg_left
         (mul_le_mul_of_nonneg_left (add_le_add hρ1 le_rfl) (by norm_num)) (by positivity)
     _ = _ := by ring
 
+open Classical in
+/-- The conditional true-heavy-count frequency bound. An empty conditioning slice has
+frequency zero, so no nonemptiness hypothesis is needed. -/
+theorem card_filter_heavyCountEvent_div_card_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) {n : ℕ} (hn : 0 < n) :
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) / #T ≤
+      2 * (1 + 4 * c * M) / ((n : ℝ) * ρ) := by
+  classical
+  have hM : 0 ≤ M := (mul_nonneg ha (sum_nonneg hd)).trans hmass
+  rcases T.eq_empty_or_nonempty with rfl | hT
+  · simp only [filter_empty, card_empty, Nat.cast_zero, zero_div]
+    positivity
+  have hTpos : (0 : ℝ) < #T := by exact_mod_cast hT.card_pos
+  exact (div_le_iff₀ hTpos).mpr
+    (card_filter_heavyCountEvent_le Y T S y ha hρ hρ1 hc hd hmass hpair hn)
+
+open Classical in
+/-- Conditioning independently on a start seed preserves the heavy-count frequency bound.
+The actual product slice is used, and either of its two factors may be empty. -/
+theorem card_filter_heavyCountEvent_product_div_card_le {Γ : Type*}
+    (Y : Ω → V → Prop) (R : Finset Γ) (T : Finset Ω) (S : Finset V) (y : V)
+    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) {n : ℕ} (hn : 0 < n) :
+    (#{σ ∈ R ×ˢ T | heavyCountEvent (fun σ w => Y σ.2 w) S d ρ n σ} : ℝ) / #(R ×ˢ T) ≤
+      2 * (1 + 4 * c * M) / ((n : ℝ) * ρ) := by
+  classical
+  refine card_filter_heavyCountEvent_div_card_le (fun (σ : Γ × Ω) w => Y σ.2 w)
+    (R ×ˢ T) S y ha hρ hρ1 hc hd hmass ?_ hn
+  intro w hw hdw hwy
+  have hset : {σ ∈ R ×ˢ T | Y σ.2 w} = R ×ˢ {σ ∈ T | Y σ w} := by
+    ext σ
+    simp [and_assoc]
+  rw [hset, card_product, card_product, Nat.cast_mul, Nat.cast_mul]
+  simpa only [mul_assoc, mul_comm, mul_left_comm] using
+    mul_le_mul_of_nonneg_left (hpair w hw hdw hwy) (Nat.cast_nonneg #R : (0 : ℝ) ≤ #R)
+
 end Cslib.Probability

Complexity/Foundations/Probability/HeavyCountRarity.lean

@@ -159,23 +159,23 @@ only the explicit conditional bound is used. This is the mean-error portion of
 [OpenAI2026LogSpace, Lemma 8.4], with an explicit constant and arbitrary positive exponent. -/
 theorem vertexNormPow_heavyCountEvent_le (hs : s ≠ 0) (hNu : 0 ≤ N * u)
     (X Y Yt : Ω → V → Prop) [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Yt σ y)]
-    {a ρ c M : ℝ} {n : ℕ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    {a ρ c M : ℝ} {n : ℕ} (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
     (hc : 0 ≤ c) (hn : 0 < n) (d : V → V → ℝ) (hd : ∀ x y, 0 ≤ d x y)
     (hmass : ∀ x, a * ∑ y, d x y ≤ M)
-    (hpair : ∀ x y w, w ≠ y →
+    (hpair : ∀ x y w, ρ / 4 < d x w → w ≠ y →
       (#{σ | X σ x ∧ Yt σ y ∧ Y σ w} : ℝ) ≤
         c * a * #{σ | X σ x ∧ Yt σ y}) (b : V → V → ℝ) :
     vertexNormPow s N u X (fun σ x =>
-      if Probability.heavyCountEvent Y (d x) ρ n σ then
+      if Probability.heavyCountEvent Y univ (d x) ρ n σ then
         kthLargest 1 {y | Yt σ y} (fun y => |b x y|) else 0) ≤
       (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) *
         rowNormPow s N u X Yt (fun _ x y => b x y) := by
   classical
   refine vertexNormPow_kthLargest_event_le hs hNu (fun x y => ?_) b
   have h := Probability.card_filter_heavyCountEvent_le Y
-    ({σ | X σ x ∧ Yt σ y} : Finset Ω) y ha hρ hρ1 hc (hd x) (hmass x)
-    (fun w hwy => ?_) hn
+    ({σ | X σ x ∧ Yt σ y} : Finset Ω) univ y ha hρ hρ1 hc (fun w _ => hd x w) (hmass x)
+    (fun w _ hdw hwy => ?_) hn
   · simpa only [filter_filter, and_assoc] using h
-  · simpa only [filter_filter, and_assoc] using hpair x y w hwy
+  · simpa only [filter_filter, and_assoc] using hpair x y w hdw hwy
 
 end Cslib

Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean

@@ -28,6 +28,8 @@ allowed. This supplies the affine-channel instance of [OpenAI2026LogSpace, Lemma
 ## Main results
 
 * `Cslib.Probability.card_heavyCountEvent_affineRetains_le`: rarity after a narrower endpoint hit.
+* `Cslib.Probability.card_heavyCountEvent_affineRetains_div_card_le`: the corresponding
+  conditional frequency, including empty slices.
 
 ## References
 
@@ -45,13 +47,14 @@ namespace Cslib.Probability
 open Classical in
 /-- The true heavy count for the actual affine channel is rare even after conditioning on
 a hit at a narrower rate. Its nominal row-mass scale is `a ^ H`, not the box side `a`. -/
-theorem card_heavyCountEvent_affineRetains_le {V : Type*} [Fintype V] {P H : ℕ}
+theorem card_heavyCountEvent_affineRetains_le {V : Type*} (S : Finset V) {P H : ℕ}
     [Fact P.Prime] {ident : V → ZMod P} (hident : Function.Injective ident)
     {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} (hLt : Lt ≤ ⌈P * a⌉₊)
     {d : V → ℝ} {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a ^ H * ∑ w, d w ≤ M) {n : ℕ} (hn : 0 < n) (y : V) :
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a ^ H * ∑ w ∈ S, d w ≤ M)
+    {n : ℕ} (hn : 0 < n) (y : V) :
     (#{s | affineRetains P H Lt s (ident y) ∧
-        heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) d ρ n s} : ℝ) ≤
+        heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) S d ρ n s} : ℝ) ≤
       (2 * (1 + 4 * (2 : ℝ) ^ H * M) / ((n : ℝ) * ρ)) *
         #{s | affineRetains P H Lt s (ident y)} := by
   classical
@@ -62,13 +65,45 @@ theorem card_heavyCountEvent_affineRetains_le {V : Type*} [Fintype V] {P H : ℕ
   have hLtP : Lt ≤ P := hLt.trans (affineRetains_rates (H := H) hPa ha).1
   simpa only [filter_filter] using card_filter_heavyCountEvent_le
     (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w))
-    ({s | affineRetains P H Lt s (ident y)} : Finset _) y
-    (pow_pos ha0 H) hρ hρ1 (by positivity : 0 ≤ (2 : ℝ) ^ H) hd hmass
-    (fun w hwy => by
+    ({s | affineRetains P H Lt s (ident y)} : Finset _) S y
+    (pow_nonneg ha0.le H) hρ hρ1 (by positivity : 0 ≤ (2 : ℝ) ^ H) hd hmass
+    (fun w _ _ hwy => by
       have h := card_affineRetains_and_affineRetains_le (H := H) hident hPa ha hLtP hwy
       convert h using 2
       congr 1
       ext s
       simp only [mem_filter, mem_univ, true_and]) hn
 
+open Classical in
+/-- The actual affine heavy-count frequency after a narrower endpoint hit. This is obtained
+from the count bound above, with zero frequency when the conditioning slice is empty. -/
+theorem card_heavyCountEvent_affineRetains_div_card_le {V : Type*} (S : Finset V) {P H : ℕ}
+    [Fact P.Prime] {ident : V → ZMod P} (hident : Function.Injective ident)
+    {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} (hLt : Lt ≤ ⌈P * a⌉₊)
+    {d : V → ℝ} {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a ^ H * ∑ w ∈ S, d w ≤ M)
+    {n : ℕ} (hn : 0 < n) (y : V) :
+    (#{s ∈ ({s | affineRetains P H Lt s (ident y)} :
+        Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))) |
+      heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) S d ρ n s} : ℝ) /
+        #{s | affineRetains P H Lt s (ident y)} ≤
+      2 * (1 + 4 * (2 : ℝ) ^ H * M) / ((n : ℝ) * ρ) := by
+  classical
+  have ha0 : 0 ≤ a := by
+    by_contra h
+    have := mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg P) (not_le.mp h).le
+    linarith
+  have hM : 0 ≤ M := (mul_nonneg (pow_nonneg ha0 H) (sum_nonneg hd)).trans hmass
+  let T : Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) :=
+    {s | affineRetains P H Lt s (ident y)}
+  change (#{s ∈ T | _} : ℝ) / #T ≤ _
+  rcases T.eq_empty_or_nonempty with hT | hT
+  · rw [hT]
+    simp only [filter_empty, card_empty, Nat.cast_zero, zero_div]
+    positivity
+  have hTpos : (0 : ℝ) < #T := by exact_mod_cast hT.card_pos
+  apply (div_le_iff₀ hTpos).mpr
+  simpa only [T, filter_filter] using
+    card_heavyCountEvent_affineRetains_le S hident hPa ha hLt hρ hρ1 hd hmass hn y
+
 end Cslib.Probability