120private lemma list_map_sum_eq_finset_sum {n : ℕ} (s : Finset (Fin n)) (f : Fin n → ℝ) : 121 (s.toList.map f).sum = s.sum f := by
proof body
Term-mode proof.
122 rw [Finset.sum_eq_multiset_sum] 123 have h1 : s.toList = Multiset.toList s.val := rfl 124 rw [h1, ← Multiset.sum_coe, ← Multiset.map_coe, Multiset.coe_toList] 125 126/-- **THEOREM**: Filtering and mapping preserves the total weight for quantum states. 127 This follows from the normalization condition of quantum states. 128 The sum of |ψᵢ|² over non-zero amplitudes equals 1 since zeros contribute nothing. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.