theorem
proved
rs_pattern_window_neutral
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Applied.PhotobiomodulationDevice on GitHub at line 216.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
213
214 Algebraically: the φ terms cancel (φ + (1-φ) + (φ-2) + (1-φ) = 0)
215 and the √2/2 terms cancel (alternating signs). -/
216theorem rs_pattern_window_neutral :
217 Finset.univ.sum rs_pattern = 0 := by
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. -/
231structure WindowNeutralPattern where
232 values : Fin 8 → ℝ
233 neutral : Finset.univ.sum values = 0
234
235/-- The RS pattern constitutes a valid window-neutral pattern. -/
236noncomputable def rs_neutral_pattern : WindowNeutralPattern :=
237 ⟨rs_pattern, rs_pattern_window_neutral⟩
238
239/-- The peak value of the pattern occurs at k=0 and equals φ. -/
240theorem rs_pattern_peak : rs_pattern ⟨0, by omega⟩ = phi := rfl
241
242/-- The φ-indexed entries (k = 0, 2, 4, 6) independently sum to zero. -/
243theorem rs_pattern_phi_components_neutral :
244 rs_pattern ⟨0, by omega⟩ + rs_pattern ⟨2, by omega⟩ +
245 rs_pattern ⟨4, by omega⟩ + rs_pattern ⟨6, by omega⟩ = 0 := by
246 simp only [rs_pattern]