From 14714b9a71fd012a55ca5605a15655c7830736a0 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:27:56 +0000 Subject: [PATCH 1/3] feat(Probability): retention by pairwise independent hashing (#1444) A point is retained when its hash lies in a target set B. Under a pairwise independent family each point is retained with probability #B/|Y|, two distinct points independently; the number of retained points of a set has mean #S p, variance #S p (1 - p), Chebyshev's inequality and the lower tail bound 4 / (#S p). Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../PairwiseIndependentHash/Retention.lean | 207 ++++++++++++++++++ ComplexityTests/PairwiseRetention.lean | 54 +++++ references.bib | 10 + 4 files changed, 272 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/Retention.lean create mode 100644 ComplexityTests/PairwiseRetention.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..3bd2f256c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2911,6 +2911,7 @@ public import Complexity.Probability.PMF.Uniform public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine +public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.Shift public import Complexity.Probability.PairwiseIndependentHash.Toeplitz public import Complexity.Probability.PairwiseIndependentHash.Universal diff --git a/Complexity/Probability/PairwiseIndependentHash/Retention.lean b/Complexity/Probability/PairwiseIndependentHash/Retention.lean new file mode 100644 index 000000000..33feb4034 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/Retention.lean @@ -0,0 +1,207 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Probability.PairwiseIndependentHash +import Complexity.Foundations.Data.Finset.Expect +import Mathlib.Algebra.Order.BigOperators.Expect + +/-! +# Retention by pairwise independent hashing + +Fix a target set `B ⊆ Y` and a pairwise independent family `h i : X → Y`. A point `x` is +*retained* by the seed `i` when its hash `h i x` lies in `B`. Each point is then retained with +probability exactly `p = #B / |Y|`, and the retention events of two distinct points are +independent: both are retained with probability exactly `p ^ 2` +(`IsPairwiseIndependentHash.expect_boole_apply_mem_and_apply_mem`). This is sampling at rate `p` +with pairwise independence, the technique of Chor and Goldreich [ChorGoldreich1989] built on the +hash families of Carter and Wegman [CarterWegman1979], [WegmanCarter1981]. For polynomial or affine +hashing over a finite field with a box `B`, the rate `p` ranges over the ratios of box size to +field size. + +The number `N i = #{x ∈ S | h i x ∈ B}` of retained points of a finite set `S` therefore has mean +`#S p`, second factorial moment `#S (#S - 1) p ^ 2` and variance `#S p (1 - p)`, and Chebyshev's +inequality bounds its deviations. In particular fewer than half of the expected number of points +are retained with probability at most `4 / (#S p)`. For a single target, `B = {y}`, these are the +cell-size moments of `Complexity.Probability.PairwiseIndependentHash`. + +## Main results + +* `Cslib.Probability.IsPairwiseIndependentHash.expect_boole_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.dens_filter_apply_mem`: a point is retained with + probability `#B / |Y|`. +* `Cslib.Probability.IsPairwiseIndependentHash.expect_boole_apply_mem_and_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.dens_filter_apply_mem_and_apply_mem`: two distinct + points are retained independently. +* `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem_mul_sub_one`, + `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem_sub_sq`: the mean, + second factorial moment and variance of the number of retained points. +* `Cslib.Probability.IsPairwiseIndependentHash.dens_le_abs_card_filter_apply_mem_sub_le`: + Chebyshev's inequality for it. +* `Cslib.Probability.IsPairwiseIndependentHash.dens_two_mul_card_filter_apply_mem_lt_le`: fewer + than half of the expected number of points are retained with probability at most `4 / (#S p)`. + +## References + +* [B. Chor, O. Goldreich, *On the power of two-point based sampling*][ChorGoldreich1989] +* [J. L. Carter, M. N. Wegman, *Universal classes of hash functions*][CarterWegman1979] +* [M. N. Wegman, J. L. Carter, *New hash functions and their use in authentication and set + equality*][WegmanCarter1981] +-/ + +public section + +namespace Cslib.Probability.IsPairwiseIndependentHash + +open Finset +open scoped BigOperators + +variable {ι X Y 𝕜 : Type*} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} + +/-- **Retention probability**: a point is retained, its hash lying in `B`, with probability +`#B / |Y|`. -/ +theorem expect_boole_apply_mem [Semifield 𝕜] [CharZero 𝕜] (hh : IsPairwiseIndependentHash h) + (x : X) (B : Finset Y) : + 𝔼 i, (if h i x ∈ B then 1 else 0 : 𝕜) = #B / Fintype.card Y := by + have hpt (i : ι) : (if h i x ∈ B then 1 else 0 : 𝕜) = ∑ y ∈ B, if h i x = y then 1 else 0 := + (sum_ite_eq B (h i x) fun _ ↦ (1 : 𝕜)).symm + simp only [hpt] + rw [expect_sum_comm] + simp only [Fintype.expect_boole, hh.dens_filter_apply_eq, NNRat.cast_inv, NNRat.cast_natCast, + sum_const, nsmul_eq_mul, div_eq_mul_inv] + +/-- **Retention probability**: a point is retained, its hash lying in `B`, with probability +`#B / |Y|`. -/ +theorem dens_filter_apply_mem (hh : IsPairwiseIndependentHash h) (x : X) (B : Finset Y) : + dens {i | h i x ∈ B} = #B / Fintype.card Y := by + have := hh.expect_boole_apply_mem (𝕜 := ℚ≥0) x B + rwa [Fintype.expect_boole, NNRat.cast_id] at this + +/-- **Pairwise independent retention**: two distinct points are retained by `B₁` and `B₂` with +probability `#B₁ / |Y| * (#B₂ / |Y|)`. -/ +theorem expect_boole_apply_mem_and_apply_mem [Semifield 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) {x₁ x₂ : X} (hx : x₁ ≠ x₂) (B₁ B₂ : Finset Y) : + 𝔼 i, (if h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + #B₁ / Fintype.card Y * (#B₂ / Fintype.card Y) := by + have hpt (i : ι) : (if h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + ∑ y₁ ∈ B₁, ∑ y₂ ∈ B₂, if h i x₁ = y₁ ∧ h i x₂ = y₂ then 1 else 0 := by + have e₂ : (if h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + ∑ y₂ ∈ B₂, if h i x₂ = y₂ then 1 else 0 := + (sum_ite_eq B₂ (h i x₂) fun _ ↦ (1 : 𝕜)).symm + rw [ite_and, ← sum_ite_eq B₁ (h i x₁) fun _ ↦ (if h i x₂ ∈ B₂ then 1 else 0 : 𝕜)] + refine sum_congr rfl fun y₁ _ ↦ ?_ + by_cases hy : h i x₁ = y₁ + · simp only [hy, true_and, ite_true] + exact e₂ + · simp [hy] + simp only [hpt] + rw [expect_sum_comm] + simp only [expect_sum_comm, Fintype.expect_boole, hh.dens_filter_apply_eq_and_apply_eq hx, + NNRat.cast_inv, NNRat.cast_pow, NNRat.cast_natCast, sum_const, nsmul_eq_mul] + ring + +/-- **Pairwise independent retention**: two distinct points are retained by `B₁` and `B₂` with +probability `#B₁ / |Y| * (#B₂ / |Y|)`. -/ +theorem dens_filter_apply_mem_and_apply_mem (hh : IsPairwiseIndependentHash h) {x₁ x₂ : X} + (hx : x₁ ≠ x₂) (B₁ B₂ : Finset Y) : + dens {i | h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂} = #B₁ / Fintype.card Y * (#B₂ / Fintype.card Y) := by + have := hh.expect_boole_apply_mem_and_apply_mem (𝕜 := ℚ≥0) hx B₁ B₂ + rwa [Fintype.expect_boole, NNRat.cast_id] at this + +/-- **The mean number of retained points** of `S` is `#S * (#B / |Y|)`. -/ +theorem expect_card_filter_apply_mem [Semifield 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) = #S * (#B / Fintype.card Y) := by + simp only [card_filter, Nat.cast_sum, Nat.cast_ite, Nat.cast_one, Nat.cast_zero] + rw [expect_sum_comm] + simp only [hh.expect_boole_apply_mem, sum_const, nsmul_eq_mul] + +/-- **The second factorial moment of the number of retained points**: the number of ordered +pairs of distinct retained points of `S` has expectation `#S (#S - 1) (#B / |Y|) ^ 2`. -/ +theorem expect_card_filter_apply_mem_mul_sub_one [Field 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) = + #S * (#S - 1) * (#B / Fintype.card Y) ^ 2 := by + classical + have hcount (i : ι) : (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) = + ∑ q ∈ S.offDiag, if h i q.1 ∈ B ∧ h i q.2 ∈ B then 1 else 0 := by + have hoff : {x ∈ S | h i x ∈ B}.offDiag = {q ∈ S.offDiag | h i q.1 ∈ B ∧ h i q.2 ∈ B} := by + ext q + simp only [mem_offDiag, mem_filter] + tauto + rw [sum_boole, ← hoff, offDiag_card, Nat.cast_sub (Nat.le_mul_self _), Nat.cast_mul] + ring + have hpair (q : X × X) (hq : q ∈ S.offDiag) : + 𝔼 i, (if h i q.1 ∈ B ∧ h i q.2 ∈ B then 1 else 0 : 𝕜) = (#B / Fintype.card Y) ^ 2 := by + rw [hh.expect_boole_apply_mem_and_apply_mem (mem_offDiag.1 hq).2.2, sq] + simp only [hcount] + rw [expect_sum_comm, sum_congr rfl hpair, sum_const, nsmul_eq_mul, offDiag_card, + Nat.cast_sub (Nat.le_mul_self _), Nat.cast_mul] + ring + +/-- **The variance of the number of retained points** is `#S p (1 - p)` with `p = #B / |Y|`. -/ +theorem expect_card_filter_apply_mem_sub_sq [Field 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2 = + #S * (#B / Fintype.card Y) * (1 - #B / Fintype.card Y) := by + have hsq (i : ι) : ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2 = + (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) + + (1 - 2 * (#S * (#B / Fintype.card Y))) * #{x ∈ S | h i x ∈ B} + + (#S * (#B / Fintype.card Y)) ^ 2 := by + ring + rcases isEmpty_or_nonempty ι with hι | hι + · rcases S.eq_empty_or_nonempty with rfl | ⟨x, -⟩ + · simp + rcases B.eq_empty_or_nonempty with rfl | ⟨y, -⟩ + · simp + exact absurd (hh.nonempty x y) (not_nonempty_iff.2 hι) + simp only [hsq, expect_add_distrib, ← mul_expect, hh.expect_card_filter_apply_mem_mul_sub_one, + hh.expect_card_filter_apply_mem, Fintype.expect_const] + ring + +/-- **Chebyshev's inequality for the number of retained points**: it is at distance at least +`ε > 0` from its mean `#S p`, with `p = #B / |Y|`, with probability at most `#S p / ε²`. -/ +theorem dens_le_abs_card_filter_apply_mem_sub_le [Field 𝕜] [LinearOrder 𝕜] + [IsStrictOrderedRing 𝕜] (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) + {ε : 𝕜} (hε : 0 < ε) : + (dens {i | ε ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)|} : 𝕜) ≤ + #S * (#B / Fintype.card Y) / ε ^ 2 := by + have hmarkov := Fintype.mul_dens_filter_le_expect + (f := fun i ↦ ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2) + (fun _ ↦ sq_nonneg _) (ε ^ 2) + simp only [sq_le_sq, abs_of_pos hε] at hmarkov + rw [le_div_iff₀ (by positivity), mul_comm] + refine hmarkov.trans ?_ + rw [hh.expect_card_filter_apply_mem_sub_sq] + have hp : (#B : 𝕜) / Fintype.card Y ≥ 0 := by positivity + exact mul_le_of_le_one_right (by positivity) (sub_le_self _ hp) + +/-- **Lower tail of the number of retained points**: fewer than half of the expected number +`#S p`, with `p = #B / |Y|`, are retained with probability at most `4 / (#S p)`. -/ +theorem dens_two_mul_card_filter_apply_mem_lt_le [Field 𝕜] [LinearOrder 𝕜] + [IsStrictOrderedRing 𝕜] (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) + (hpos : 0 < (#S : 𝕜) * (#B / Fintype.card Y)) : + (dens {i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < #S * (#B / Fintype.card Y)} : 𝕜) ≤ + 4 / (#S * (#B / Fintype.card Y)) := by + set μ : 𝕜 := #S * (#B / Fintype.card Y) + have hsub : ({i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < μ} : Finset ι) ⊆ + ({i | μ / 2 ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - μ|} : Finset ι) := by + intro i hi + simp only [mem_filter, mem_univ, true_and] at hi ⊢ + rw [abs_sub_comm, abs_of_pos (by linarith)] + linarith + calc (dens {i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < μ} : 𝕜) + ≤ (dens {i | μ / 2 ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - μ|} : 𝕜) := by + exact_mod_cast dens_le_dens hsub + _ ≤ μ / (μ / 2) ^ 2 := hh.dens_le_abs_card_filter_apply_mem_sub_le S B (by positivity) + _ = 4 / μ := by + field_simp + ring + +end Cslib.Probability.IsPairwiseIndependentHash diff --git a/ComplexityTests/PairwiseRetention.lean b/ComplexityTests/PairwiseRetention.lean new file mode 100644 index 000000000..bb4a35fe5 --- /dev/null +++ b/ComplexityTests/PairwiseRetention.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Probability.KWiseIndependent.Polynomial +import Complexity.Probability.PairwiseIndependentHash.Retention +import Mathlib.Algebra.Field.ZMod + +/-! +# Retention by polynomial hashing + +Polynomial hashing `x ↦ c₀ + c₁ x` over `𝔽₅`, retaining a point when its hash lies in the box +`{0, 1}`: a point is retained at rate `2 / 5`, as a direct count over the `25` seeds confirms; +two distinct points are retained jointly at rate `4 / 25`; and all five points have `2` retained +on average. +-/ + +namespace ComplexityTests.PairwiseRetention + +open Cslib Cslib.Probability Finset +open scoped BigOperators + +private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ + +private theorem hp : + IsPairwiseIndependentHash (polynomialHash : (Fin 2 → ZMod 5) → ZMod 5 → ZMod 5) := + (isKWiseIndependentHash_polynomialHash 2).isPairwiseIndependentHash le_rfl + +-- Each point is retained at rate `2 / 5`. +example (x : ZMod 5) : dens {c : Fin 2 → ZMod 5 | polynomialHash c x ∈ ({0, 1} : Finset _)} = + 2 / 5 := by + rw [hp.dens_filter_apply_mem, show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +-- The same rate, counted directly: `10` of the `25` seeds retain the point `3`. +example : #{c : Fin 2 → ZMod 5 | polynomialHash c 3 ∈ ({0, 1} : Finset _)} = 10 := by decide + +-- Two distinct points are both retained at rate `4 / 25`. +example : dens {c : Fin 2 → ZMod 5 | + polynomialHash c 0 ∈ ({0, 1} : Finset _) ∧ polynomialHash c 1 ∈ ({0, 1} : Finset _)} = + 4 / 25 := by + rw [hp.dens_filter_apply_mem_and_apply_mem (by decide), + show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +-- Of all five points, `2` are retained on average. +example : 𝔼 c : Fin 2 → ZMod 5, + (#{x ∈ (univ : Finset (ZMod 5)) | polynomialHash c x ∈ ({0, 1} : Finset _)} : ℚ) = 2 := by + rw [hp.expect_card_filter_apply_mem, show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +end ComplexityTests.PairwiseRetention diff --git a/references.bib b/references.bib index ffd09ecfe..ec215b3f7 100644 --- a/references.bib +++ b/references.bib @@ -1050,6 +1050,16 @@ @article{ChorGoldreich1988 doi = {10.1137/0217015} } +@article{ChorGoldreich1989, + author = {Chor, Benny and Goldreich, Oded}, + title = {On the Power of Two-Point Based Sampling}, + journal = {Journal of Complexity}, + volume = {5}, + number = {1}, + pages = {96--106}, + year = {1989} +} + @article{ChungGrahamFranklShearer1986, author = {Chung, Fan R. K. and Graham, Ronald L. and Frankl, Peter and Shearer, James B.}, title = {Some Intersection Theorems for Ordered Sets and Graphs}, From 4943d9b0e91fa86788863e3fa7a211187d386748 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:57:30 +0000 Subject: [PATCH 2/3] feat(Probability): affine retention channels over a prime field (#1682) Identifiers y : ZMod P are retained when A y + b lies in the box {v | all coordinates < L} of ZMod P ^ H. Exact rates (L/P)^H and their squares for pairs, the lower tail 4/(#A pi), independence of separate seeds, and the assembled channel properties at rate f = a^H with L = ceil(P a): f <= pi <= 2^H f. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../RetentionChannel.lean | 212 ++++++++++++++++++ ComplexityTests/RetentionChannel.lean | 56 +++++ 3 files changed, 269 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean create mode 100644 ComplexityTests/RetentionChannel.lean diff --git a/Complexity.lean b/Complexity.lean index 3bd2f256c..957459612 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2912,6 +2912,7 @@ public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine public import Complexity.Probability.PairwiseIndependentHash.Retention +public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel public import Complexity.Probability.PairwiseIndependentHash.Shift public import Complexity.Probability.PairwiseIndependentHash.Toeplitz public import Complexity.Probability.PairwiseIndependentHash.Universal diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean new file mode 100644 index 000000000..b890a5bad --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -0,0 +1,212 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Probability.PairwiseIndependentHash.Affine +public import Complexity.Probability.PairwiseIndependentHash.Retention +public import Mathlib.Algebra.Field.ZMod +public import Mathlib.Algebra.Order.Archimedean.Real.Basic +import Mathlib.Data.Fintype.BigOperators + +/-! +# Retention channels over a prime field + +A *retention channel* selects a random set of identifiers at a prescribed rate, with pairwise +independence. Its seed is an affine map `y ↦ A y + b` from `𝔽_P` to `𝔽_P ^ H`, with a uniformly +random matrix `A` and vector `b`. The identifier `y : ZMod P` is *retained* +(`affineRetains P H L s y`) when every coordinate of `A y + b`, read as a number in +`{0, …, P - 1}`, is less than `L`. The target is then the box `retentionBox P H L` with `L ^ H` +points (`card_retentionBox`). By the pairwise independence of affine hashing +(`isPairwiseIndependentHash_affineHash`) and the general retention bounds of +`Complexity.Probability.PairwiseIndependentHash.Retention`, every identifier is retained with +probability exactly `π = (L / P) ^ H`, and two distinct identifiers both with probability `π ^ 2`. +This is sampling by pairwise independent hashing [ChorGoldreich1989] with the hash families of +Carter and Wegman [CarterWegman1979]. + +For a target rate `f = a ^ H` with `1 ≤ P a` and `a ≤ 1`, the side `L = ⌈P a⌉` gives +`f ≤ π ≤ 2 ^ H f` (`affineRetains_rates`). Then the conditional probability that `w` is +retained, given that `y ≠ w` is retained, is at most `2 ^ H f`. A deterministic nonempty set `A` +retains fewer than `#A π / 2` of its identifiers with probability at most `4 / (#A π)`. Two +channels with independent seeds, on the product seed space, give independent events +(`dens_filter_fst_and_snd`). + +These are the channel properties used in Section 4 of the OpenAI preprint *Exact +Derandomization of Logarithmic Space* (2026, unrefereed): there, `c_π f ≤ π_f ≤ C_π f`, +`Pr[Y(w) | Y(y)] ≤ C_pair f`, the lower tail `Pr[∑_{x ∈ A} X(x) < |A| π / 2] ≤ C_var / (|A| π)`, +and the independence of the channels `X` and `Y`. Here the constants are `c_π = 1`, +`C_π = C_pair = 2 ^ H` and `C_var = 4`. The preprint conditions its channels on linearly +independent frames, which changes these constants only by a bounded factor. The frames matter +only for the later averaging walks, so they are not needed here. + +## Main definitions + +* `Cslib.Probability.retentionBox`: the box `{v | ∀ j, (v j).val < L}` in `ZMod P ^ H`. +* `Cslib.Probability.affineRetains`: the identifier `y` is retained by the affine seed `s`. + +## Main results + +* `Cslib.Probability.card_retentionBox`: the box has `L ^ H` points. +* `Cslib.Probability.dens_affineRetains`, `Cslib.Probability.dens_affineRetains_and`: exact + retention probabilities of one identifier and of two distinct ones. +* `Cslib.Probability.dens_two_mul_card_filter_affineRetains_lt_le`: the lower tail of the number + of retained identifiers of a set. +* `Cslib.Probability.dens_filter_fst_and_snd`: events about independent seeds are independent. +* `Cslib.Probability.affineRetains_rates`: the four channel properties at rate `f = a ^ H`. + +## References + +* [B. Chor, O. Goldreich, *On the power of two-point based sampling*][ChorGoldreich1989] +* [J. L. Carter, M. N. Wegman, *Universal classes of hash functions*][CarterWegman1979] +-/ + +public section + +namespace Cslib.Probability + +open Finset +open scoped BigOperators + +/-- **Independence of separate seeds**: on the product of two seed spaces, an event about the +first seed and an event about the second have probability equal to the product of their +probabilities. -/ +theorem dens_filter_fst_and_snd {ι κ : Type*} [Fintype ι] [Fintype κ] (p : ι → Prop) + (q : κ → Prop) [DecidablePred p] [DecidablePred q] : + dens {z : ι × κ | p z.1 ∧ q z.2} = dens {i | p i} * dens {j | q j} := by + rw [dens_eq_card_div_card, dens_eq_card_div_card, dens_eq_card_div_card, + ← univ_product_univ, filter_product, card_product, Fintype.card_prod] + push_cast + rw [mul_div_mul_comm] + +variable (P H L : ℕ) [NeZero P] + +/-- The **retention box** `{v | ∀ j, (v j).val < L}` in `ZMod P ^ H`: every coordinate, read as +a number in `{0, …, P - 1}`, is less than `L`. -/ +def retentionBox : Finset (Fin H → ZMod P) := + Fintype.piFinset fun _ ↦ {a : ZMod P | a.val < L} + +variable {P H L} + +/-- `L` residues of `ZMod P` have representatives less than `L ≤ P`. -/ +private theorem card_filter_val_lt (hL : L ≤ P) : #{a : ZMod P | a.val < L} = L := by + have himage : ({a : ZMod P | a.val < L} : Finset (ZMod P)).image ZMod.val = range L := by + ext k + simp only [mem_image, mem_filter, mem_univ, true_and, mem_range] + refine ⟨fun ⟨a, ha, hak⟩ ↦ hak ▸ ha, fun hk ↦ ⟨k, ?_, ?_⟩⟩ <;> + rw [ZMod.val_cast_of_lt (by omega)] + exact hk + calc #({a : ZMod P | a.val < L} : Finset (ZMod P)) + = #(({a : ZMod P | a.val < L} : Finset (ZMod P)).image ZMod.val) := + (card_image_of_injective _ (ZMod.val_injective P)).symm + _ = L := by rw [himage, card_range] + +/-- The retention box has `L ^ H` points when `L ≤ P`. -/ +theorem card_retentionBox (hL : L ≤ P) : #(retentionBox P H L) = L ^ H := by + rw [retentionBox, Fintype.card_piFinset, prod_const, card_univ, Fintype.card_fin, + card_filter_val_lt hL] + +variable (P H L) + +/-- The identifier `y` is **retained** by the affine seed `s = (A, b)` when `A y + b` lies in the +retention box. -/ +abbrev affineRetains (s : Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) (y : ZMod P) : + Prop := + affineHash s (fun _ ↦ y) ∈ retentionBox P H L + +variable {P H L} [Fact P.Prime] + +/-- The affine hash of identifiers is pairwise independent. -/ +private theorem isPairwiseIndependentHash_affineIdentifier : + IsPairwiseIndependentHash fun (s : Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) + (y : ZMod P) ↦ affineHash s (fun _ ↦ y) := + isPairwiseIndependentHash_affineHash.comp (e := fun y _ ↦ y) fun _ _ h ↦ congrFun h 0 + +/-- **Retention probability**: every identifier is retained with probability `(L / P) ^ H`. -/ +theorem dens_affineRetains (hL : L ≤ P) (y : ZMod P) : + dens {s | affineRetains P H L s y} = ((L : ℚ≥0) / P) ^ H := by + have h := isPairwiseIndependentHash_affineIdentifier.dens_filter_apply_mem y + (retentionBox P H L) + rw [card_retentionBox hL, Fintype.card_fun, Fintype.card_fin, ZMod.card] at h + unfold affineRetains + rw [h, div_pow] + push_cast + rfl + +/-- **Pairwise independent retention**: two distinct identifiers are both retained with +probability `((L / P) ^ H) ^ 2`. -/ +theorem dens_affineRetains_and (hL : L ≤ P) {w y : ZMod P} (hwy : w ≠ y) : + dens {s | affineRetains P H L s w ∧ affineRetains P H L s y} = + ((L : ℚ≥0) / P) ^ H * ((L : ℚ≥0) / P) ^ H := by + have h := isPairwiseIndependentHash_affineIdentifier.dens_filter_apply_mem_and_apply_mem hwy + (retentionBox P H L) (retentionBox P H L) + rw [card_retentionBox hL, Fintype.card_fun, Fintype.card_fin, ZMod.card] at h + unfold affineRetains + rw [h, div_pow] + push_cast + rfl + +/-- **Lower tail of the retained count**: a set `A` of identifiers retains fewer than half of its +expected number `#A π`, with `π = (L / P) ^ H`, with probability at most `4 / (#A π)`. -/ +theorem dens_two_mul_card_filter_affineRetains_lt_le (hL : L ≤ P) (A : Finset (ZMod P)) + (hpos : 0 < (#A : ℝ) * ((L : ℝ) / P) ^ H) : + (dens {s | 2 * (#{y ∈ A | affineRetains P H L s y} : ℝ) < #A * ((L : ℝ) / P) ^ H} : ℝ) ≤ + 4 / (#A * ((L : ℝ) / P) ^ H) := by + have hrate : ((#(retentionBox P H L) : ℝ) / Fintype.card (Fin H → ZMod P)) = + ((L : ℝ) / P) ^ H := by + rw [card_retentionBox hL, Fintype.card_fun, Fintype.card_fin, ZMod.card, div_pow] + push_cast + rfl + have h := isPairwiseIndependentHash_affineIdentifier.dens_two_mul_card_filter_apply_mem_lt_le + (𝕜 := ℝ) A (retentionBox P H L) (by rwa [hrate]) + rw [hrate] at h + exact h + +/-- **The four channel properties at rate `f = a ^ H`.** Let `1 ≤ P a`, `a ≤ 1` and +`L = ⌈P a⌉`, and write `π = (L / P) ^ H` for the retention probability. Then `L ≤ P`, +`f ≤ π ≤ 2 ^ H f`, two distinct identifiers are both retained with probability at most +`2 ^ H f` times the probability that one of them is, and a nonempty set `A` retains fewer than +`#A π / 2` of its identifiers with probability at most `4 / (#A π)`. Independence of two channels +is `dens_filter_fst_and_snd`. -/ +theorem affineRetains_rates {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) : + let L := ⌈P * a⌉₊ + L ≤ P ∧ a ^ H ≤ ((L : ℝ) / P) ^ H ∧ ((L : ℝ) / P) ^ H ≤ 2 ^ H * a ^ H ∧ + (∀ w y : ZMod P, w ≠ y → + (dens {s | affineRetains P H L s w ∧ affineRetains P H L s y} : ℝ) ≤ + 2 ^ H * a ^ H * dens {s | affineRetains P H L s y}) ∧ + ∀ A : Finset (ZMod P), A.Nonempty → + (dens {s | 2 * (#{y ∈ A | affineRetains P H L s y} : ℝ) < #A * ((L : ℝ) / P) ^ H} : + ℝ) ≤ 4 / (#A * ((L : ℝ) / P) ^ H) := by + intro L + have hP : (0 : ℝ) < P := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne P) + have ha0 : 0 < a := by + by_contra h + have := mul_nonpos_of_nonneg_of_nonpos hP.le (not_lt.1 h) + linarith + have hLlo : (P : ℝ) * a ≤ L := Nat.le_ceil _ + have hLhi : (L : ℝ) ≤ 2 * (P * a) := by + have := Nat.ceil_lt_add_one (by positivity : (0 : ℝ) ≤ P * a) + linarith + have hLP : L ≤ P := Nat.ceil_le.2 (by nlinarith) + have hlo : a ≤ (L : ℝ) / P := by + rw [le_div_iff₀ hP] + linarith + have hhi : (L : ℝ) / P ≤ 2 * a := by + rw [div_le_iff₀ hP] + linarith + have hrate_hi : ((L : ℝ) / P) ^ H ≤ 2 ^ H * a ^ H := by + rw [← mul_pow] + exact pow_le_pow_left₀ (by positivity) hhi H + refine ⟨hLP, pow_le_pow_left₀ ha0.le hlo H, hrate_hi, fun w y hwy ↦ ?_, fun A hA ↦ ?_⟩ + · rw [dens_affineRetains_and hLP hwy, dens_affineRetains hLP] + push_cast + exact mul_le_mul_of_nonneg_right hrate_hi (by positivity) + · refine dens_two_mul_card_filter_affineRetains_lt_le hLP A ?_ + have : (0 : ℝ) < #A := by exact_mod_cast hA.card_pos + have : 0 < (L : ℝ) / P := ha0.trans_le hlo + positivity + +end Cslib.Probability diff --git a/ComplexityTests/RetentionChannel.lean b/ComplexityTests/RetentionChannel.lean new file mode 100644 index 000000000..9f278970a --- /dev/null +++ b/ComplexityTests/RetentionChannel.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Probability.PairwiseIndependentHash.RetentionChannel + +/-! +# Retention channels over a prime field + +A retention channel over `𝔽₅` with one coordinate and side `2` retains each identifier at rate +`2 / 5`. A direct count over its `25` seeds confirms the rate. Two independent channels retain two +given identifiers jointly at rate `(2 / 5) ^ 2`. Over `𝔽₇` in two coordinates, at target rate +`f = (1 / 2) ^ 2`, the channel properties hold with side `L = ⌈7 / 2⌉ = 4`. +-/ + +namespace ComplexityTests.RetentionChannel + +open Cslib Cslib.Probability Finset + +private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ +private instance : Fact (Nat.Prime 7) := ⟨by decide⟩ + +-- The box `{0, 1}` in `𝔽₅`, and the exact retention rate `2 / 5`. +example : #(retentionBox 5 1 2) = 2 := card_retentionBox (by norm_num) + +example (y : ZMod 5) : dens {s | affineRetains 5 1 2 s y} = 2 / 5 := by + rw [dens_affineRetains (by norm_num)] + norm_num + +-- A direct count: `10` of the `25` seeds `(A, b)` retain the identifier `3`. +example : #{s | affineRetains 5 1 2 s 3} = 10 := by decide + +-- Two independent channels, on the product seed space, retain `3` in the first and `4` in the +-- second with probability `(2 / 5) * (2 / 5)`. +example : dens {z : (Matrix (Fin 1) (Fin 1) (ZMod 5) × (Fin 1 → ZMod 5)) × + (Matrix (Fin 1) (Fin 1) (ZMod 5) × (Fin 1 → ZMod 5)) | + affineRetains 5 1 2 z.1 3 ∧ affineRetains 5 1 2 z.2 4} = 4 / 25 := by + have h := dens_filter_fst_and_snd (fun s ↦ affineRetains 5 1 2 s 3) + (fun s ↦ affineRetains 5 1 2 s 4) + rw [dens_affineRetains (by norm_num), dens_affineRetains (by norm_num)] at h + convert h using 1 + norm_num + +-- At rate `f = (1 / 2) ^ 2` over `𝔽₇`, the side is `L = ⌈7 / 2⌉ = 4`, and the retention rate +-- `(4 / 7) ^ 2` lies within `[f, 4 f]`. +example : (1 / 2 : ℝ) ^ 2 ≤ ((4 : ℝ) / 7) ^ 2 ∧ ((4 : ℝ) / 7) ^ 2 ≤ 2 ^ 2 * (1 / 2 : ℝ) ^ 2 := by + obtain ⟨-, hlo, hhi, -, -⟩ := + affineRetains_rates (P := 7) (H := 2) (a := 1 / 2) (by norm_num) (by norm_num) + have hceil : ⌈((7 : ℕ) : ℝ) * (1 / 2)⌉₊ = 4 := by norm_num [Nat.ceil_eq_iff] + rw [hceil] at hlo hhi + push_cast at hlo hhi + exact ⟨hlo, hhi⟩ + +end ComplexityTests.RetentionChannel From 6fc88dbc5340163284cf9bf752651b879a0970c9 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 04:00:24 -0400 Subject: [PATCH 3/3] doc(Probability): cite the pinned retention-channel source --- .../PairwiseIndependentHash/RetentionChannel.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean index b890a5bad..7b243567c 100644 --- a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -35,8 +35,8 @@ retains fewer than `#A π / 2` of its identifiers with probability at most `4 / channels with independent seeds, on the product seed space, give independent events (`dens_filter_fst_and_snd`). -These are the channel properties used in Section 4 of the OpenAI preprint *Exact -Derandomization of Logarithmic Space* (2026, unrefereed): there, `c_π f ≤ π_f ≤ C_π f`, +These are the channel properties used in Section 4 of the unrefereed preprint +[OpenAI2026LogSpace]: there, `c_π f ≤ π_f ≤ C_π f`, `Pr[Y(w) | Y(y)] ≤ C_pair f`, the lower tail `Pr[∑_{x ∈ A} X(x) < |A| π / 2] ≤ C_var / (|A| π)`, and the independence of the channels `X` and `Y`. Here the constants are `c_π = 1`, `C_π = C_pair = 2 ^ H` and `C_var = 4`. The preprint conditions its channels on linearly @@ -62,6 +62,7 @@ only for the later averaging walks, so they are not needed here. * [B. Chor, O. Goldreich, *On the power of two-point based sampling*][ChorGoldreich1989] * [J. L. Carter, M. N. Wegman, *Universal classes of hash functions*][CarterWegman1979] +* [OpenAI, *Exact Derandomization of Logarithmic Space*][OpenAI2026LogSpace] -/ public section