Documentation

Mathlib.Data.Nat.BitIndices

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 in 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.

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

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

Equations
Instances For
    source
    @[simp]
    theorem Nat.bitIndices_zero :
    Nat.bitIndices 0 = []
    source
    @[simp]
    theorem Nat.bitIndices_one :
    Nat.bitIndices 1 = [0]
    source
    theorem Nat.bitIndices_bit_true (n : ℕ) :
    (Nat.bit true n).bitIndices = 0 :: List.map (fun (x : ℕ) => x + 1) n.bitIndices
    source
    theorem Nat.bitIndices_bit_false (n : ℕ) :
    (Nat.bit false n).bitIndices = List.map (fun (x : ℕ) => x + 1) n.bitIndices
    source
    @[simp]
    theorem Nat.bitIndices_two_mul_add_one (n : ℕ) :
    (2 * n + 1).bitIndices = 0 :: List.map (fun (x : ℕ) => x + 1) n.bitIndices
    source
    @[simp]
    theorem Nat.bitIndices_two_mul (n : ℕ) :
    (2 * n).bitIndices = List.map (fun (x : ℕ) => x + 1) n.bitIndices
    source
    @[simp]
    theorem Nat.bitIndices_sorted {n : ℕ} :
    List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) n.bitIndices
    source
    @[simp]
    theorem Nat.bitIndices_two_pow_mul (k : ℕ) (n : ℕ) :
    (2 ^ k * n).bitIndices = List.map (fun (x : ℕ) => x + k) n.bitIndices
    source
    @[simp]
    theorem Nat.bitIndices_two_pow (k : ℕ) :
    (2 ^ k).bitIndices = [k]
    source
    @[simp]
    theorem Nat.twoPowSum_bitIndices (n : ℕ) :
    (List.map (fun (i : ℕ) => 2 ^ i) n.bitIndices).sum = n
    source
    @[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.

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