50lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) : 51 sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
proof body
Tactic-mode proof.
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 61 simpa using this 62 63end PatternLayer 64 65namespace MeasurementLayer 66 67open scoped BigOperators 68open Finset PatternLayer 69 70/-- Sum of one 8‑tick sub‑block starting at index `j*8`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.