Lengths of encoded lists

The framed encoding of a list (Turing.MultiTapeTM.encList) spends 2 * |enc a| + 1 symbols on each element a. In particular the sum of the lengths of its encoded elements is no longer than the encoding, as is the list itself (Turing.MultiTapeTM.length_le_length_encList). Such bounds are what a reduction needs to bound the size of its output, or a verifier the length of a certificate, in terms of the input.

Main results

• Turing.MultiTapeTM.length_encList: the exact length.
• Turing.MultiTapeTM.sum_length_le_length_encList: the encoded elements are no longer, in total, than the encoded list.
• Turing.MultiTapeTM.length_encList_set_le: bound on the encoded length after replacing a list element.
• Turing.MultiTapeTM.length_unframe_add_dropFrame_le: the unframed prefix and remaining suffix of any bit list satisfy 2 * (unframe v).length + (dropFrame v).length ≤ v.length.

theorem Turing.MultiTapeTM.length_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : ((encList enc) l).length = (List.map (fun (a : α) => 2 * (enc a).length + 1) l).sum

@[simp]

theorem Turing.MultiTapeTM.length_encList_reverse {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : ((encList enc) l.reverse).length = ((encList enc) l).length

Reversing a list preserves the full encoded size, including each element's framing.

theorem Turing.MultiTapeTM.sum_length_le_length_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : (List.map (fun (a : α) => (enc a).length) l).sum ≤ ((encList enc) l).length

The encoded elements of a list are no longer, in total, than the encoded list.

theorem Turing.MultiTapeTM.length_encList_set_le {α : Type u_1} (enc : α ↪ List Bool) (l : List α) (i : ℕ) (x : α) : ((encList enc) (l.set i x)).length ≤ ((encList enc) l).length + 2 * (enc x).length + 1

Replacing an element of a list increases the encoded list length by at most 2 * (enc x).length + 1.

theorem Turing.MultiTapeTM.length_unframe_add_dropFrame_le (v : List Bool) : 2 * (unframe v).length + (dropFrame v).length ≤ v.length

The unframed prefix and remaining suffix of any bit list satisfy 2 * (unframe v).length + (dropFrame v).length ≤ v.length.