ModularRows.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The modular pivot order of a pair-stream row

These are the two cyclic orders in lem:streams. The list is an analysis view of one sorted slice: implementation can traverse the slice by its pivot and cursor, rather than allocating the reordered list. The permutation theorems preserve occurrence multiplicity, including repeated residues.

def OAI.LowSpaceSubsetSum.ModularRows.direct line 22
def OAI.LowSpaceSubsetSum.ModularRows.complementary line 26
theorem OAI.LowSpaceSubsetSum.ModularRows.direct_perm line 30
theorem OAI.LowSpaceSubsetSum.ModularRows.complementary_perm line 35
theorem OAI.LowSpaceSubsetSum.ModularRows.direct_wrapped line 40
theorem OAI.LowSpaceSubsetSum.ModularRows.direct_unwrapped line 46
theorem OAI.LowSpaceSubsetSum.ModularRows.complementary_low line 50
theorem OAI.LowSpaceSubsetSum.ModularRows.complementary_high line 54

theorem OAI.LowSpaceSubsetSum.ModularRows.direct_sorted line 60

Source documentation

Direct cyclic traversal is sorted by normalized pair residue.

theorem direct_sorted {P r : ℤ} (hr : 0 ≤ r) (hrP : r < P)
    (residue : α → ℤ) (xs : List α)
    (hbound : ∀ x ∈ xs, 0 ≤ residue x ∧ residue x < P)
    (hsort : xs.Pairwise (fun x y => residue x ≤ residue y)) :
    (direct P r residue xs).Pairwise
      (fun x y => (r + residue x) % P ≤ (r + residue y) % P) := by
…

Mentions: OAI.LowSpaceSubsetSum.ModularRows.direct

theorem OAI.LowSpaceSubsetSum.ModularRows.complementary_sorted line 95

Source documentation

Reverse cyclic traversal is sorted by the complementary residue.

theorem complementary_sorted {P K : ℤ} (hK : 0 ≤ K) (hKP : K < P)
    (residue : α → ℤ) (xs : List α)
    (hbound : ∀ x ∈ xs, 0 ≤ residue x ∧ residue x < P)
    (hsort : xs.Pairwise (fun x y => residue x ≤ residue y)) :
    (complementary K residue xs).Pairwise
      (fun x y => (K - residue x) % P ≤ (K - residue y) % P) := by
…

Mentions: OAI.LowSpaceSubsetSum.ModularRows.complementary

theorem OAI.LowSpaceSubsetSum.ModularRows.filtered_sorted line 129

Source documentation

Filtering a row by the small modulus preserves its residue ordering.

theorem filtered_sorted (p c : ℤ) (weight residue : α → ℤ) (xs : List α)
    (hsort : xs.Pairwise (fun x y => residue x ≤ residue y)) :
    (xs.filter (fun x => decide (weight x % p = c % p))).Pairwise
      (fun x y => residue x ≤ residue y) := hsort.filter _
…

Mentions: OAI.LowSpaceSubsetSum.weight