CompressionConcentration.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The compressed-block trial's high-deficiency partition event

The sample space is the actual uniform permutation of input indices. Each of the seven blocks is marginally uniform; independence between blocks is never assumed. The floor in the retained block-list capacity is included.

theorem OAI.LowSpaceSubsetSum.permutation_deficiency_tail line 21

theorem OAI.LowSpaceSubsetSum.compression_partition_good_probability line 32

Source documentation

Exact seven-block union bound in the high-mean case.

theorem compression_partition_good_probability {n s : ℕ} (hn : 0 < n)
    (hs : (s : ℝ) ≤ (3 / 25 : ℝ) * n)
    (a : Fin n → ℤ) (K : Fin 7 → Finset (Fin n)) (hK : ∀ i, (K i).card = s)
    (hmean : (153 / 20000 : ℝ) * n ≤ meanDeficiency a Finset.univ s) :
    1 - (84000000 : ℝ) / n ≤ finiteUniformProbability (fun e : Equiv.Perm (Fin n) =>
      ∀ i, (151 / 20000 : ℝ) * n ≤ deficiency a (permuteSubset e (K i))) := by
…

Mentions: OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.deficiency, OAI.LowSpaceSubsetSum.permuteSubset

def OAI.LowSpaceSubsetSum.compressionCapExponent line 79
theorem OAI.LowSpaceSubsetSum.compression_block_size_test line 82
theorem OAI.LowSpaceSubsetSum.compression_size_tests_probability line 101
Source documentation
The actual seven size tests pass with probability at least one half for an absolute explicit threshold. This is only the partition event, before prime sampling and the solution-bucket argument.
```
theorem compression_size_tests_probability {n : ℕ} (hn : 168000000 ≤ n)
    (a : Fin n → ℤ) (K : Fin 7 → Finset (Fin n))
    (hK : ∀ i, (K i).card = mixerSize n / 2)
    (hmean : (153 / 20000 : ℝ) * n ≤
      meanDeficiency a Finset.univ (mixerSize n / 2)) :
    (1 / 2 : ℝ) ≤ finiteUniformProbability (fun e : Equiv.Perm (Fin n) =>
      ∀ i, distinctSumCount a (permuteSubset e (K i)) ≤ 2 ^ compressionCapExponent n) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.mixerSize, OAI.LowSpaceSubsetSum.meanDeficiency, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.permuteSubset, OAI.LowSpaceSubsetSum.compressionCapExponent