nonzero_card_three

formal source

 137/-- At `D = 3`, the non-zero count is `7`. The seven Booker plot
 138    families bijection in `Aesthetics.NarrativeGeodesic` chains off
 139    this corollary. -/
 140theorem nonzero_card_three :
 141    (Finset.univ.filter (fun v : F2Power 3 => v ≠ 0)).card = 7 := by
 142  have h := @nonzero_card 3
 143  -- h : … = 2 ^ 3 - 1
 144  have h2 : (2 : ℕ) ^ 3 - 1 = 7 := by norm_num
 145  rw [h2] at h
 146  exact h
 147
 148/-! ## Hamming weight -/
 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