Bit Indices

Given n : ℕ, we define Nat.bitIndices n, which is the List of indices of 1s in the binary expansion of n. If s : Finset ℕ and n = ∑ i ∈ s, 2^i, then Nat.bitIndices n is the sorted list of elements of s.

The lemma twoPowSum_bitIndices proves that summing 2 ^ i over this list gives n. This is used in Combinatorics.colex to construct a bijection equivBitIndices : ℕ ≃ Finset ℕ.

TODO

Relate the material in this file to Nat.digits and Nat.bits.

def Nat.bitIndices (n : ℕ) : List ℕ

The function which maps each natural number ∑ i ∈ s, 2^i to the list of elements of s in increasing order.

Equations

• n.bitIndices = Nat.binaryRec [] (fun (b : Bool) (x : ℕ) (s : List ℕ) => Bool.casesOn b (List.map (fun (x : ℕ) => x + 1) s) (0 :: List.map (fun (x : ℕ) => x + 1) s)) n

@[simp]

theorem Nat.bitIndices_zero : bitIndices 0 = []

@[simp]

theorem Nat.bitIndices_one : bitIndices 1 = [0]

theorem Nat.bitIndices_bit_true (n : ℕ) : (bit true n).bitIndices = 0 :: List.map (fun (x : ℕ) => x + 1) n.bitIndices

theorem Nat.bitIndices_bit_false (n : ℕ) : (bit false n).bitIndices = List.map (fun (x : ℕ) => x + 1) n.bitIndices

@[simp]

theorem Nat.bitIndices_two_mul_add_one (n : ℕ) : (2 * n + 1).bitIndices = 0 :: List.map (fun (x : ℕ) => x + 1) n.bitIndices

@[simp]

theorem Nat.bitIndices_two_mul (n : ℕ) : (2 * n).bitIndices = List.map (fun (x : ℕ) => x + 1) n.bitIndices

@[simp]

theorem Nat.bitIndices_sorted {n : ℕ} : List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) n.bitIndices

@[simp]

theorem Nat.bitIndices_two_pow_mul (k n : ℕ) : (2 ^ k * n).bitIndices = List.map (fun (x : ℕ) => x + k) n.bitIndices

@[simp]

theorem Nat.bitIndices_two_pow (k : ℕ) : (2 ^ k).bitIndices = [k]

@[simp]

theorem Nat.twoPowSum_bitIndices (n : ℕ) : (List.map (fun (i : ℕ) => 2 ^ i) n.bitIndices).sum = n

@[irreducible]

theorem Nat.bitIndices_twoPowsum {L : List ℕ} (hL : List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) L) : (List.map (fun (i : ℕ) => 2 ^ i) L).sum.bitIndices = L

Together with Nat.twoPowSum_bitIndices, this implies a bijection between ℕ and Finset ℕ. See Finset.equivBitIndices for this bijection.

theorem Nat.two_pow_le_of_mem_bitIndices {a n : ℕ} (ha : a ∈ n.bitIndices) : 2 ^ a ≤ n

theorem Nat.not_mem_bitIndices_self (n : ℕ) : n ∉ n.bitIndices