OAI/Combinatorics/LowSpaceSubsetSum/Streams/RecordedJoin.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LowSpaceSubsetSum.RecordedDictionary.matchingRecords line 12

   Source documentation

   A proof view; the runtime never constructs this Cartesian list.

   def matchingRecords (key₁ : β → ℤ) (key₂ : γ → ℤ) (emit : β → γ → Option α)
       (xs : List β) (ys : List γ) : List α :=
   …

2. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.mem_matchingRecords line 16
3. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.matchFold_eq_records line 28
4. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.fold_provenance line 42
5. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.matchFold_fits line 51
6. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.join_eq_records line 78
7. theorem OAI.LowSpaceSubsetSum.RecordedDictionary.join_provenance line 98

   Source documentation

   No capacity hypothesis is needed for provenance: overflowing joins retain only entries emitted by a matching pair.

   theorem join_provenance {σ₁ σ₂ : Type*} (C : ℕ) (encode : α → List Bool)
       (read₁ : σ₁ → Option (β × σ₁)) (key₁ : β → ℤ)
       (read₂ : σ₂ → Option (γ × σ₂)) (key₂ : γ → ℤ) (emit : β → γ → Option α)
       (view₁ : σ₁ → List β) (hread₁ : RowMerge.IsReader read₁ view₁)
       (view₂ : σ₂ → List γ) (hread₂ : RowMerge.IsReader read₂ view₂)
       (B fuel₁ fuel₂ controlFuel : ℕ) (s₁ : σ₁) (s₂ : σ₂)
       (hsort₁ : (view₁ s₁).Pairwise (fun x y => key₁ x ≤ key₁ y))
       (hsort₂ : (view₂ s₂).Pairwise (fun x y => key₂ x ≤ key₂ y))
       (hcap₁ : (view₁ s₁).length ≤ fuel₁) (hcap₂ : (view₂ s₂).length ≤ fuel₂)
       (hfuel : (view₁ s₁).length + (view₂ s₂).length < controlFuel)
       (z : α) (hz : z ∈ (StreamJoin.stopped read₁ key₁ read₂ key₂ (callback C encode emit)
         B fuel₁ fuel₂ controlFuel s₁ s₂ empty).state.user.records.toList) :
   …

   Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.StreamJoin.stopped, OAI.LowSpaceSubsetSum.RecordedDictionary.callback, OAI.LowSpaceSubsetSum.RecordedDictionary.empty