English
Let L be a finite list of natural numbers that is strictly increasing. Then the sum of 2^i over i in L has bitIndices equal to L.
Русский
Пусть L — конечный список натуральных чисел, упорядоченный по возрастанию. Тогда сумма 2^i по i из L имеет битовые индексы, равные L.
LaTeX
$$$\forall L \in \mathrm{List}(\mathbb{N}), \ \mathrm{List.Sorted}(L, <) \Rightarrow \bigg( \big( \sum_{i \in L} 2^{i} \big).\mathrm{bitIndices} = L \bigg)$$$
Lean4
/-- Together with `Nat.twoPowSum_bitIndices`, this implies a bijection between `ℕ` and `Finset ℕ`.
See `Finset.equivBitIndices` for this bijection. -/
theorem bitIndices_twoPowsum {L : List ℕ} (hL : List.Sorted (· < ·) L) : (L.map (fun i ↦ 2 ^ i)).sum.bitIndices = L :=
by
cases L with
| nil => simp
| cons a L =>
obtain ⟨haL, hL⟩ := sorted_cons.1 hL
simp_rw [Nat.lt_iff_add_one_le] at haL
have h' : ∃ (L₀ : List ℕ), L₀.Sorted (· < ·) ∧ L = L₀.map (· + a + 1) :=
by
refine ⟨L.map (· - (a + 1)), ?_, ?_⟩
· rwa [Sorted, pairwise_map, Pairwise.and_mem, Pairwise.iff (S := fun x y ↦ x ∈ L ∧ y ∈ L ∧ x < y), ←
Pairwise.and_mem]
simp only [and_congr_right_iff]
exact fun x y hx _ ↦ by rw [tsub_lt_tsub_iff_right (haL _ hx)]
have h' : ∀ x ∈ L, ((fun x ↦ x + a + 1) ∘ (fun x ↦ x - (a + 1))) x = x := fun x hx ↦ by
simp only [add_assoc, Function.comp_apply]; rw [tsub_add_cancel_of_le (haL _ hx)]
simp [List.map_congr_left h']
obtain ⟨L₀, hL₀, rfl⟩ := h'
have hrw : (2 ^ ·) ∘ (· + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i) := by ext x;
simp only [Function.comp_apply, pow_add, pow_one]; ac_rfl
simp only [List.map_cons, List.map_map, List.sum_map_mul_left, List.sum_cons, hrw]
nth_rw 1 [← mul_one (a := 2 ^ a)]
rw [← mul_add, bitIndices_two_pow_mul, add_comm, bitIndices_two_mul_add_one, bitIndices_twoPowsum hL₀]
simp [add_comm (a := 1), add_assoc]
termination_by L.length
