Blocks of bit strings

The repeated sampler of thm:parallel-repetition presents k copies of an input CL function on 𝔽₂^s as one CL function on 𝔽₂^{k s} (CLFun.famSum, along finProdFinEquiv), and its program handles vectors as bit strings cut into k consecutive blocks of s bits (Data.chunk). This module relates the two: the bits of a joined vector are the concatenation of the bits of its blocks (toBits_join), the i-th block of the vector read off a bit string is the vector read off the i-th chunk (block_ofBits), and likewise for indicator strings of register subspaces (indicatorBits_blockSet).

theorem MIPRE.CL.finProdFinEquiv_val {k s : ℕ} (i : Fin k) (j : Fin s) : ↑(finProdFinEquiv (i, j)) = ↑j + s * ↑i

theorem MIPRE.CL.ofFn_eq_flatten_blocks {k s : ℕ} {α : Type u_1} (f : Fin (k * s) → α) : List.ofFn f = (List.ofFn fun (i : Fin k) => List.ofFn fun (j : Fin s) => f (finProdFinEquiv (i, j))).flatten

A list indexed by Fin (k s) is the concatenation of its k blocks of s.

theorem MIPRE.CL.toBits_join {k s : ℕ} (v : Fin k → Fin s → 𝔽₂) : toBits (join finProdFinEquiv v) = (List.ofFn fun (i : Fin k) => toBits (v i)).flatten

The bits of a joined vector: the bits of its blocks, concatenated.

theorem MIPRE.CL.indicatorBits_blockSet {k s : ℕ} (T : Fin k → Finset (Fin s)) : indicatorBits (blockSet finProdFinEquiv T) = (List.ofFn fun (i : Fin k) => indicatorBits (T i)).flatten

The indicator string of a block set: the indicator strings of the blocks, concatenated.

theorem MIPRE.CL.length_flatten_ofFn {k s : ℕ} {α : Type u_1} (g : Fin k → List α) (hg : ∀ (i : Fin k), (g i).length = s) : (List.ofFn g).flatten.length = k * s

theorem MIPRE.CL.chunk_flatten_ofFn {s : ℕ} {α : Type u_1} {k : ℕ} (g : Fin k → List α) : (∀ (i : Fin k), (g i).length = s) → ∀ (i : Fin k), Cost.Data.chunk s (↑i) (List.ofFn g).flatten = g i

The i-th chunk of a concatenation of k lists of length s is the i-th list.

theorem MIPRE.CL.block_ofBits {k s : ℕ} (z : Cost.BitStr) (i : Fin k) : block finProdFinEquiv i (ofBits (k * s) z) = ofBits s (Cost.Data.chunk s (↑i) z)

The i-th block of the vector read off a bit string is the vector read off its i-th chunk.

theorem MIPRE.CL.chunk_map {s : ℕ} {α : Type u_1} {β : Type u_2} (f : α → β) (i : ℕ) (l : List α) : Cost.Data.chunk s i (List.map f l) = List.map f (Cost.Data.chunk s i l)

@[simp]

theorem MIPRE.CL.chunk_zero {s : ℕ} {α : Type u_1} (l : List α) : Cost.Data.chunk s 0 l = List.take s l

theorem MIPRE.CL.chunk_succ {s : ℕ} {α : Type u_1} (i : ℕ) (l : List α) : Cost.Data.chunk s (i + 1) l = Cost.Data.chunk s i (List.drop s l)

theorem MIPRE.CL.length_chunk {k s : ℕ} {α : Type u_1} {l : List α} (hl : l.length = k * s) (i : Fin k) : (Cost.Data.chunk s (↑i) l).length = s

@[simp]

theorem MIPRE.CL.chunk_nil {s : ℕ} {α : Type u_1} (i : ℕ) : Cost.Data.chunk s i [] = []

def MIPRE.Cost.Data.bitsOf (l : List Data) : BitStr

The bits denoted by a list of data (bitOf), the left inverse of encoding a bit string.

Equations

• MIPRE.Cost.Data.bitsOf l = List.map MIPRE.Cost.Data.bitOf l

@[simp]

theorem MIPRE.Cost.Data.bitsOf_map_ofBool (x : BitStr) : bitsOf (List.map ofBool x) = x

theorem MIPRE.Cost.Data.encode_nat_eq_list (n : ℕ) : encode n = list (List.map ofBool n.bits)

theorem MIPRE.Cost.Data.toList_encode_bitStr (x : BitStr) : (encode x).toList = List.map ofBool x

theorem MIPRE.Cost.Data.replicate_nil_eq_map (m : ℕ) : List.replicate m nil = List.map ofBool (List.replicate m false)