extendPeriodic8

formal source

  27  { s | ∀ i : Fin n, s i.val = w i }
  28
  29/-- Periodic extension of an 8‑bit window. -/
  30def extendPeriodic8 (w : Pattern 8) : Stream := fun t =>
  31  let i : Fin 8 := ⟨t % 8, Nat.mod_lt _ (by decide)⟩
  32  w i
  33
  34/-- Sum of the first `m` bits of a stream. -/
  35def sumFirst (m : Nat) (s : Stream) : Nat :=
  36  ∑ i : Fin m, (if s i.val then 1 else 0)
  37
  38/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/
  39lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
  40  {s : Stream} (hs : s ∈ Cylinder w) :
  41  sumFirst n s = Z_of_window w := by
  42  classical
  43  unfold sumFirst Z_of_window Cylinder at *
  44  have : (fun i : Fin n => (if s i.val then 1 else 0)) =
  45         (fun i : Fin n => (if w i then 1 else 0)) := by
  46    funext i; simpa [hs i]
  47  simpa [this]
  48
  49/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
  50lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  51  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  52  classical
  53  unfold sumFirst Z_of_window extendPeriodic8
  54  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
  55    intro i; exact Nat.mod_eq_of_lt i.isLt
  56  have hfun :
  57    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
  58    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
  59      funext i; simp [hmod i]
  60  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun