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 sum_map_two_pow_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 : ℕ} : n.bitIndices.SortedLT

@[simp]

theorem Nat.bitIndices_nodup {n : ℕ} : n.bitIndices.Nodup

@[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.sum_map_two_pow_bitIndices (n : ℕ) : (List.map (fun (i : ℕ) => 2 ^ i) n.bitIndices).sum = n

@[deprecated Nat.sum_map_two_pow_bitIndices (since := "2026-05-15")]

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

Alias of Nat.sum_map_two_pow_bitIndices.

@[simp]

theorem Nat.mem_bitIndices {i n : ℕ} : i ∈ n.bitIndices ↔ n.testBit i = true

theorem Nat.bitIndices_sum_map_two_pow {L : List ℕ} (hL : L.SortedLT) : (List.map (fun (i : ℕ) => 2 ^ i) L).sum.bitIndices = L

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

@[deprecated Nat.bitIndices_sum_map_two_pow (since := "2026-05-15")]

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

Alias of Nat.bitIndices_sum_map_two_pow.

---

Together with Nat.sum_map_bitIndices_two_pow, 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.notMem_bitIndices_self (n : ℕ) : ¬n ∈ n.bitIndices