  83  simp [this]
  84
  85/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
  86lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  87  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  88  classical
  89  unfold sumFirst Z_of_window extendPeriodic8
  90  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
  91    intro i; exact Nat.mod_eq_of_lt i.isLt
  92  have h8 : 0 < 8 := by decide
  93  have hfun :
  94    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ h8⟩ then 1 else 0))
  95    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
  96      funext i; simp [hmod i]
  97  -- Now the two sums are definitionally equal by hfun.
  98  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
  99  simpa using this
 100
 101lemma extendPeriodic8_in_cylinder (w : Pattern 8) : (extendPeriodic8 w) ∈ (Cylinder w) := by
 102  intro i
 103  dsimp [extendPeriodic8, Cylinder]
 104  have hmod : (i.val % 8) = i.val := Nat.mod_eq_of_lt i.isLt
 105  simp [hmod]
 106
 107lemma sumFirst_nonneg (m : Nat) (s : Stream) : 0 ≤ sumFirst m s := by
 108  unfold sumFirst
 109  apply Finset.sum_nonneg
 110  intro i _
 111  split
 112  · norm_num
 113  · norm_num
 114
 115lemma sumFirst_eq_zero_of_all_false {m : Nat} {s : Stream}
 116  (h : ∀ i : Fin m, s i.val = false) :

papers checked against this theorem

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