FixedBuckets.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Overflow probability for one fixed solution bucket

Equal actual weights are separated before prime collision estimates. A finite set of weight--mask keys may contain many keys with the same weight; linearity of expectation counts every such key when its weight differs from the fixed solution's weight. This is the bucket argument in both trial analyses.

def OAI.LowSpaceSubsetSum.sameWeightKeys line 20
def OAI.LowSpaceSubsetSum.otherCollisionKeys line 23
def OAI.LowSpaceSubsetSum.hashBucket line 27
theorem OAI.LowSpaceSubsetSum.hashBucket_card line 30
theorem OAI.LowSpaceSubsetSum.expected_otherCollisionKeys_le line 44

theorem OAI.LowSpaceSubsetSum.probability_count_le line 71

Source documentation

Weighted finite Markov for any nonnegative counted quantity.

theorem probability_count_le (seeds : Finset Ω) (prob : Ω → ℝ) (count : Ω → ℕ)
    (hnonneg : ∀ ω ∈ seeds, 0 ≤ prob ω) (hprob : ∑ ω ∈ seeds, prob ω = 1)
    {M T : ℝ} (hT : 0 < T)
    (hmean : (∑ ω ∈ seeds, prob ω * count ω) ≤ M) :
    1 - M / T ≤ ∑ ω ∈ seeds.filter (fun ω => (count ω : ℝ) ≤ T), prob ω := by
…

theorem OAI.LowSpaceSubsetSum.fixed_bucket_fits_probability line 106

theorem OAI.LowSpaceSubsetSum.prime_fixed_bucket_fits_probability line 137

Source documentation

Concrete extra-prime bucket success. The equal-weight capacity premise is supplied separately by the mask-counting lemmas in Buckets.

theorem prime_fixed_bucket_fits_probability (X : Finset α) (value : α → ℤ)
    {x : α} (hx : x ∈ X) {ell u C : ℕ} (hell : 4 ≤ ell) (hellu : ell ≤ u)
    (hC : 0 < C) (hequal : ((sameWeightKeys X value x).card : ℝ) ≤ (C : ℝ) / 2)
    (hbits : ∀ y ∈ X, ∀ z ∈ X, (value y - value z).natAbs < 2 ^ (2 * u)) :
    1 - 16 * (u : ℝ) ^ 2 * X.card / ((C : ℝ) * (2 : ℝ) ^ ell) ≤
      ∑ p ∈ (primeRange ell).filter
        (fun (p : ℕ) => (hashBucket X value (fun w => w % (p : ℤ)) x).card ≤ C),
          primeProbability ell p := by
…

Mentions: OAI.LowSpaceSubsetSum.sameWeightKeys, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.hashBucket, OAI.LowSpaceSubsetSum.primeProbability