extendPeriodic8

formal source

  26abbrev Cylinder {n : Nat} (w : Pattern n) : Set Stream := PatternLayer.Cylinder w
  27
  28/-- Periodic extension of an 8-bit window. -/
  29abbrev extendPeriodic8 := PatternLayer.extendPeriodic8
  30
  31/-- Sum of the first `m` bits of a stream. -/
  32abbrev sumFirst (m : Nat) (s : Stream) : Nat := PatternLayer.sumFirst m s
  33
  34/-- Sum of one 8-tick sub-block starting at index `j * 8`. -/
  35abbrev subBlockSum8 (s : Stream) (j : Nat) : Nat := MeasurementLayer.subBlockSum8 s j
  36
  37/-- Aligned block sum over `k` copies of the 8-tick window. -/
  38abbrev blockSumAligned8 (k : Nat) (s : Stream) : Nat := MeasurementLayer.blockSumAligned8 k s
  39
  40/-- Averaged (per-window) observation over aligned blocks. -/
  41abbrev observeAvg8 (k : Nat) (s : Stream) : Nat := MeasurementLayer.observeAvg8 k s
  42
  43/-- On any stream lying in the cylinder of an 8-bit window, the first block sum equals `Z`. -/
  44lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
  45    (hs : s ∈ Cylinder w) :
  46    subBlockSum8 s 0 = Z_of_window w := by
  47  simpa [subBlockSum8, Cylinder, Z_of_window]
  48    using MeasurementLayer.firstBlockSum_eq_Z_on_cylinder (w:=w) (s:=s) hs
  49
  50/-- For periodic extensions of an 8-bit window, each sub-block sums to `Z`. -/
  51lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
  52    subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
  53  simpa [subBlockSum8, extendPeriodic8, Z_of_window]
  54    using MeasurementLayer.subBlockSum8_periodic_eq_Z (w:=w) j
  55
  56/-- For `s = extendPeriodic8 w`, summing `k` aligned 8-blocks yields `k * Z(w)`. -/
  57lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
  58    blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
  59  simpa [blockSumAligned8, extendPeriodic8, Z_of_window]