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.

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
    theorem Nat.bitIndices_bit_true (n : ) :
    (Nat.bit true n).bitIndices = 0 :: List.map (fun (x : ) => x + 1) n.bitIndices
    theorem Nat.bitIndices_bit_false (n : ) :
    (Nat.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 : ) :
    nn.bitIndices