OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionBucket.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.direct_complementary_residue line 10
2. theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftPair_mem line 23
3. theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftSolution_pair line 31
4. theorem OAI.LowSpaceSubsetSum.CompressionSetup.rightSolution_pair line 40
5. def OAI.LowSpaceSubsetSum.CompressionSetup.solutionResidue line 49
6. theorem OAI.LowSpaceSubsetSum.CompressionSetup.solutionResidue_val line 52
7. theorem OAI.LowSpaceSubsetSum.CompressionSetup.finiteResidue_reduced line 56
8. def OAI.LowSpaceSubsetSum.CompressionSetup.leftBucket line 60
9. theorem OAI.LowSpaceSubsetSum.CompressionSetup.solutionBucket_fits line 63
10. def OAI.LowSpaceSubsetSum.CompressionSetup.leftDictionary line 68
11. theorem OAI.LowSpaceSubsetSum.CompressionSetup.leftDictionary_fits line 75
12. def OAI.LowSpaceSubsetSum.CompressionSetup.DictionarySuccess line 111
13. theorem OAI.LowSpaceSubsetSum.CompressionSetup.dictionarySuccess_probability line 117
14. theorem OAI.LowSpaceSubsetSum.CompressionSetup.generated_left_dictionary line 129

    Source documentation

    The generated sorted readers may permute occurrences, but their exact group-list membership suffices for the actual join to retain the solution.

    theorem generated_left_dictionary {σ₀ σ₁ : Type*}
        (e : Equiv.Perm (Fin n)) (q : PrimeSpace n) (hq : R.BucketFits e q)
        (read₀ : σ₀ → Option (ℤ × σ₀)) (read₁ : σ₁ → Option (ℤ × σ₁))
        (view₀ : σ₀ → List ℤ) (hread₀ : RowMerge.IsReader read₀ view₀)
        (view₁ : σ₁ → List ℤ) (hread₁ : RowMerge.IsReader read₁ view₁)
        (s₀ : σ₀) (s₁ : σ₁)
        (hview₀ : ∀ x, x ∈ view₀ s₀ ↔ x ∈ R.groupList e 0)
        (hview₁ : ∀ x, x ∈ view₁ s₁ ↔ x ∈ R.groupList e 1)
        (B fuel₀ fuel₁ controlFuel : ℕ)
        (hsort₀ : (view₀ s₀).Pairwise (fun x y => x % (q.val : ℤ) ≤ y % q.val))
        (hsort₁ : (view₁ s₁).Pairwise (fun x y =>
          (((R.solutionResidue e q).val : ℤ) - x) % q.val ≤
    …

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.RowMerge.IsReader

15. theorem OAI.LowSpaceSubsetSum.CompressionSetup.generated_right_hit line 183

    Source documentation

    Once the left dictionary contains the fixed left weight, the actual right readers find its complementary exact weight in the same residue pass.

    theorem generated_right_hit {σ₂ σ₃ : Type*}
        (e : Equiv.Perm (Fin n)) (q : PrimeSpace n) (tree : BinaryTrie.Tree)
        (hleft : BinaryTrie.contains tree (WeightEncoding.weightKey R.input (R.leftWeight e)) = true)
        (read₂ : σ₂ → Option (ℤ × σ₂)) (read₃ : σ₃ → Option (ℤ × σ₃))
        (view₂ : σ₂ → List ℤ) (hread₂ : RowMerge.IsReader read₂ view₂)
        (view₃ : σ₃ → List ℤ) (hread₃ : RowMerge.IsReader read₃ view₃)
        (s₂ : σ₂) (s₃ : σ₃)
        (hview₂ : ∀ x, x ∈ view₂ s₂ ↔ x ∈ R.groupList e 2)
        (hview₃ : ∀ x, x ∈ view₃ s₃ ↔ x ∈ R.groupList e 3)
        (B fuel₂ fuel₃ controlFuel : ℕ)
        (hsort₂ : (view₂ s₂).Pairwise (fun x y => x % (q.val : ℤ) ≤ y % q.val))
        (hsort₃ : (view₃ s₃).Pairwise (fun x y =>
    …

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup.PrimeSpace, OAI.LowSpaceSubsetSum.BinaryTrie.Tree, OAI.LowSpaceSubsetSum.BinaryTrie.contains, OAI.LowSpaceSubsetSum.WeightEncoding.weightKey, OAI.LowSpaceSubsetSum.RowMerge.IsReader