pith. machine review for the scientific record. sign in
lemma proved tactic proof

observeAvg8_periodic_eq_Z

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 142lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
 143  observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by

proof body

Tactic-mode proof.

 144  classical
 145  unfold observeAvg8
 146  have hsum := blockSumAligned8_periodic w k
 147  have : (k * Z_of_window w) / k = Z_of_window w := by
 148    exact Nat.mul_div_cancel_left (Z_of_window w) (Nat.pos_of_ne_zero hk)
 149  simpa [hsum, this]
 150
 151end MeasurementLayer
 152
 153/-! ## Examples (witnesses) -/
 154namespace Examples
 155
 156open PatternLayer MeasurementLayer
 157
 158/-- Example 8‑bit window: ones at even indices (Z=4). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.