RepresentationBucketCapacity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Capacity of the actual designated parent buckets

theorem OAI.LowSpaceSubsetSum.hashBucket_mod_mul_low line 13

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenParentBucket_eq_hashBucket line 31

Source documentation

The low restriction removes no member of the full product-modulus bucket.

theorem chosenParentBucket_eq_hashBucket (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (j : Fin 2) (q : ℕ) :
    R.chosenParentBucket h r hn hlog j ((prefixModulus h.2.val 0 : ℤ) * q) =
      hashBucket (R.chosenLowEntries h r hn hlog j) Entry.value
        (fun w => w % ((prefixModulus h.2.val 0 : ℤ) * q))
        (RepresentationUniverse.entry (R.signedWeights h.1.1.1)
          (R.chosenRawParent h r hn hlog j)) := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.hashBucket, OAI.LowSpaceSubsetSum.RepresentationUniverse.entry

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLeftBucket_fits line 57

Source documentation

The unrefined left bucket fits its actual fixed-capacity dictionary.

theorem chosenLeftBucket_fits (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (q : ℕ)
    (hq : ((R.chosenOtherBucket h r hn hlog 0 q).card : ℝ) ≤
      (compressionDictionaryCapacity n : ℝ) / 2) :
    (R.chosenParentBucket h r hn hlog 0 ((prefixModulus h.2.val 0 : ℤ) * q)).card ≤
      compressionDictionaryCapacity n := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity, OAI.LowSpaceSubsetSum.prefixModulus

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenRightFullBucket_fits line 79

Source documentation

A full right-mask prefix has one possible equal-weight key, while its unequal-weight keys are already counted in the unrefined collision bucket.

theorem chosenRightFullBucket_fits (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment hn hlog)) h r)
    (q : ℕ) (D : Finset (Fin n))
    (hq : ((R.chosenOtherBucket h r hn hlog 1 q).card : ℝ) ≤
      (compressionDictionaryCapacity n : ℝ) / 2) :
    ((R.chosenParentBucket h r hn hlog 1 ((prefixModulus h.2.val 0 : ℤ) * q)).filter
      (fun e => e.mask = D)).card ≤ compressionDictionaryCapacity n := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity, OAI.LowSpaceSubsetSum.prefixModulus

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBuckets_probability line 129

Source documentation

Both actual bucket capacities hold for at least nine tenths of the extra prime choices, with no independence assumption between the two counts.

theorem chosenBuckets_probability (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 20000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment (by omega) hlog)) h r)
    (hgood : R.AllocatedResourceGood hn hlog ⟨h, r⟩)
    (hs : mixerSpreadTest (R.signedWeights h.1.1.1) (R.orderedMixers h.1.1.1) n)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
    (D : Finset (Fin n)) :
    (9 / 10 : ℝ) ≤
      ∑ q ∈ (primeRange (R.extraPrimeParameter h.1.1.1)).filter (fun q : ℕ =>
        (R.chosenParentBucket h r (by omega) hlog 0 ((prefixModulus h.2.val 0 : ℤ) * q)).card ≤
          compressionDictionaryCapacity n ∧
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.mixerSpreadTest, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity

abbrev OAI.LowSpaceSubsetSum.RepresentationSetup.ExtraPrimeSpace line 165
Source documentation
The extra-prime draw is uniform on the concrete prime range.
```
abbrev ExtraPrimeSpace (z : Layout n) := ↥(primeRange (R.extraPrimeParameter z))
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.primeRange
def OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeLaw line 167
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeLaw_probability line 173

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenBuckets_law_probability line 186

Source documentation

Finite-kernel version of the two actual dictionary-capacity bounds.

theorem chosenBuckets_law_probability (h : R.PrimeHistory) (r : R.Residues h.2)
    (hn : 20000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000)
    (hr : R.ResidueSuccess (R.actualOffsets (R.allocatedChildAssignment (by omega) hlog)) h r)
    (hgood : R.AllocatedResourceGood hn hlog ⟨h, r⟩)
    (hs : mixerSpreadTest (R.signedWeights h.1.1.1) (R.orderedMixers h.1.1.1) n)
    (hscale : Real.logb 2 (inputScale R.input : ℝ) ≤ (n : ℝ) / 1000000000)
    (D : Finset (Fin n)) :
    (9 / 10 : ℝ) ≤ (R.extraPrimeLaw h.1.1.1 (by omega)).probability (fun q =>
        (R.chosenParentBucket h r (by omega) hlog 0 ((prefixModulus h.2.val 0 : ℤ) * q.val)).card ≤
          compressionDictionaryCapacity n ∧
        ((R.chosenParentBucket h r (by omega) hlog 1 ((prefixModulus h.2.val 0 : ℤ) * q.val)).filter
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.mixerSpreadTest, OAI.LowSpaceSubsetSum.inputScale, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.compressionDictionaryCapacity