pith. machine review for the scientific record. sign in
theorem proved term proof

rs_pattern_window_neutral

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)

 216theorem rs_pattern_window_neutral :
 217    Finset.univ.sum rs_pattern = 0 := by

proof body

Term-mode proof.

 218  rw [Finset.sum_fin_eq_sum_range]
 219  simp only [Finset.sum_range_succ, Finset.sum_range_zero, rs_pattern]
 220  rw [dif_pos (show (0 : ℕ) < 8 by omega),
 221      dif_pos (show (1 : ℕ) < 8 by omega),
 222      dif_pos (show (2 : ℕ) < 8 by omega),
 223      dif_pos (show (3 : ℕ) < 8 by omega),
 224      dif_pos (show (4 : ℕ) < 8 by omega),
 225      dif_pos (show (5 : ℕ) < 8 by omega),
 226      dif_pos (show (6 : ℕ) < 8 by omega),
 227      dif_pos (show (7 : ℕ) < 8 by omega)]
 228  ring
 229
 230/-- A window-neutral modulation pattern for an 8-tick cycle. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.