`Stream`

definition

show as: view math explainer →

module: IndisputableMonolith.Streams
domain: Streams
line: 11 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Streams on GitHub at line 11.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   8open Classical
   9
  10/-- Boolean stream as an infinite display. -/
  11def Stream := Nat → Bool
  12
  13/-- A finite window/pattern of length `n`. -/
  14def Pattern (n : Nat) := Fin n → Bool
  15
  16/-- Integer functional `Z` counting ones in a finite window. -/
  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. -/

papers checked against this theorem

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