RepresentationBucketProbability.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual low-entry universes and extra-prime collision expectations

theorem OAI.LowSpaceSubsetSum.residueFiltered_eq_mod_filter line 13
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLowEntries line 26
Source documentation
The actual distinct-entry universe after only the parent low filter.
```
def chosenLowEntries (h : R.PrimeHistory) (r : R.Residues h.2) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) (j : Fin 2) :
    Finset (Entry (Fin n)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.Entry
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLowEntries_subset line 35
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenEntry_lowEntries line 42
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLowEntries_card line 53
def OAI.LowSpaceSubsetSum.RepresentationSetup.chosenOtherBucket line 83
Source documentation
Different-weight entries in the designated full parent bucket.
```
def chosenOtherBucket (h : R.PrimeHistory) (r : R.Residues h.2) (hn : 10000 ≤ n)
    (hlog : Real.logb 2 ((mixerSize n : ℝ) + 1) + 1 ≤ (n : ℝ) / 1000) (j : Fin 2) (q : ℕ) :
    Finset (Entry (Fin n)) :=
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.Entry

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenOtherBucket_expectation line 92

Source documentation

Linearity of expectation counts actual distinct keys, including repeated weights with different masks. The nonzero differences meet the input bit bound.

theorem chosenOtherBucket_expectation (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 ∈ primeRange (R.extraPrimeParameter h.1.1.1),
      primeProbability (R.extraPrimeParameter h.1.1.1) q *
        (R.chosenOtherBucket h r hn hlog j q).card) ≤
      (inputScale R.input : ℝ) ^ 3 / (2 : ℝ) ^ R.extraPrimeRate h.1.1.1 *
        (R.chosenLowEntries h r hn hlog j).card := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.primeProbability, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenLowEntries_resource_bound line 111

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenOtherBucket_resource_expectation line 125

Source documentation

The resource event bounds each designated different-weight bucket expectation by u^203 2^(Lambda-x).

theorem chosenOtherBucket_resource_expectation (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⟩) (j : Fin 2) :
    (∑ q ∈ primeRange (R.extraPrimeParameter h.1.1.1),
      primeProbability (R.extraPrimeParameter h.1.1.1) q *
        (R.chosenOtherBucket h r (by omega) hlog j q).card) ≤
      (inputScale R.input : ℝ) ^ 203 *
        (2 : ℝ) ^ (R.resourceLambda h.1.1.1 h.1.1.2 - R.extraPrimeRate h.1.1.1) := by
…

Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.primeRange, OAI.LowSpaceSubsetSum.primeProbability, OAI.LowSpaceSubsetSum.inputScale

theorem OAI.LowSpaceSubsetSum.RepresentationSetup.chosenOtherBuckets_probability line 147

Source documentation

Both different-weight counts are controlled by one finite Markov bound; there is no independence assertion between the two parent sides.

theorem chosenOtherBuckets_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⟩) :
    1 - 4 * (inputScale R.input : ℝ) ^ 203 *
        (2 : ℝ) ^ (R.resourceLambda h.1.1.1 h.1.1.2 - R.extraPrimeRate h.1.1.1) /
          (compressionDictionaryCapacity n : ℝ) ≤
      ∑ q ∈ (primeRange (R.extraPrimeParameter h.1.1.1)).filter (fun q =>
        ((R.chosenOtherBucket h r (by omega) hlog 0 q).card : ℝ) ≤
          (compressionDictionaryCapacity n : ℝ) / 2 ∧
        ((R.chosenOtherBucket h r (by omega) hlog 1 q).card : ℝ) ≤
…

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