 149
 150/-- The Hamming weight of `v`: the number of coordinates equal to
 151    `true`. -/
 152def hammingWeight (v : F2Power D) : ℕ :=
 153  (Finset.univ.filter (fun i => v i = true)).card
 154
 155@[simp] theorem hammingWeight_zero : hammingWeight (0 : F2Power D) = 0 := by
 156  unfold hammingWeight
 157  simp [zero_apply]
 158
 159theorem hammingWeight_le (v : F2Power D) : hammingWeight v ≤ D := by
 160  unfold hammingWeight
 161  calc (Finset.univ.filter (fun i => v i = true)).card
 162      ≤ Finset.univ.card := Finset.card_filter_le _ _
 163    _ = D := by simp [Finset.card_univ, Fintype.card_fin]
 164
 165theorem weight_zero_iff (v : F2Power D) :
 166    hammingWeight v = 0 ↔ v = 0 := by
 167  constructor
 168  · intro h
 169    unfold hammingWeight at h
 170    rw [Finset.card_eq_zero] at h
 171    funext i
 172    have hi : i ∉ Finset.univ.filter (fun j => v j = true) := by
 173      rw [h]; exact Finset.notMem_empty _
 174    simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi
 175    -- hi : ¬ v i = true
 176    cases hv : v i
 177    · rfl
 178    · exact absurd hv hi
 179  · intro h
 180    subst h
 181    exact hammingWeight_zero
 182

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.