Z_of_window_nonneg

formal source

  17def Z_of_window {n : Nat} (w : Pattern n) : Nat :=
  18  ∑ i : Fin n, (if w i then 1 else 0)
  19
  20lemma Z_of_window_nonneg {n : Nat} (w : Pattern n) : 0 ≤ Z_of_window w := by
  21  unfold Z_of_window
  22  apply Finset.sum_nonneg
  23  intro i _
  24  split <;> decide
  25
  26@[simp] lemma Z_of_window_zero (w : Pattern 0) : Z_of_window w = 0 := by
  27  simp [Z_of_window]
  28
  29/-- The cylinder set of streams whose first `n` bits coincide with the window `w`. -/
  30def Cylinder {n : Nat} (w : Pattern n) : Set Stream :=
  31  { s | ∀ i : Fin n, s i.val = w i }
  32
  33@[simp] lemma mem_Cylinder_zero (w : Pattern 0) (s : Stream) : s ∈ Cylinder w := by
  34  intro i; exact (Fin.elim0 i)
  35
  36@[simp] lemma Cylinder_zero (w : Pattern 0) : Cylinder w = Set.univ := by
  37  ext s; constructor
  38  · intro _; exact Set.mem_univ _
  39  · intro _; exact (mem_Cylinder_zero w s)
  40
  41/-- Periodic extension of an 8‑bit window. -/
  42def extendPeriodic8 (w : Pattern 8) : Stream := fun t =>
  43  let h8 : 0 < 8 := by decide
  44  let i : Fin 8 := ⟨t % 8, Nat.mod_lt _ h8⟩
  45  w i
  46
  47@[simp] lemma extendPeriodic8_zero (w : Pattern 8) : extendPeriodic8 w 0 = w ⟨0, by decide⟩ := by
  48  simp [extendPeriodic8]
  49
  50@[simp] lemma extendPeriodic8_eq_mod (w : Pattern 8) (t : Nat) :