twoPowSum_bitIndices — Mathlib

English

The sum of 2^i over i in bitIndices(n) equals n; i.e., ∑_{i ∈ bitIndices(n)} 2^i = n.

Русский

Сумма 2^i по i ∈ bitIndices(n) равна n; то есть ∑_{i ∈ bitIndices(n)} 2^i = n.

LaTeX

$$$\sum_{i \in n.bitIndices} 2^i = n$$$

Lean4

@[simp]
theorem twoPowSum_bitIndices (n : ℕ) : (n.bitIndices.map (fun i ↦ 2 ^ i)).sum = n := by
  induction n using binaryRec with
  | zero => simp
  | bit b n
    hs =>
    have hrw : (fun i ↦ 2 ^ i) ∘ (fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i := by ext i; simp [pow_add, mul_comm]
    cases b
    · simpa [hrw, List.sum_map_mul_left]
    simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]

Похожие утверждения