IndisputableMonolith.Cost.Ndim.Octave

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Octave (`n=8`) coefficient trajectories
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11/-- Uniform phase shift for an octave index. -/
  12noncomputable def octavePhase (i : Fin 8) : ℝ := 2 * Real.pi * (i : ℝ) / 8
  13
  14/-- Phase-shifted cosine trajectory used in the `n=8` visualization. -/
  15noncomputable def octaveTrajectory (amp t : ℝ) : Vec 8 :=
  16  fun i => amp * Real.cos (t + octavePhase i)
  17
  18theorem octaveTrajectory_periodic (amp t : ℝ) :
  19    octaveTrajectory amp (t + 2 * Real.pi) = octaveTrajectory amp t := by
  20  ext i
  21  unfold octaveTrajectory
  22  have hrew : t + 2 * Real.pi + octavePhase i = (t + octavePhase i) + 2 * Real.pi := by ring
  23  calc
  24    amp * Real.cos (t + 2 * Real.pi + octavePhase i)
  25        = amp * Real.cos ((t + octavePhase i) + 2 * Real.pi) := by rw [hrew]
  26    _ = amp * Real.cos (t + octavePhase i) := by
  27          rw [Real.cos_add_two_pi]
  28
  29end Ndim
  30end Cost
  31end IndisputableMonolith
  32