theorem
proved
tactic proof
octaveTrajectory_periodic
show as:
view Lean formalization →
formal statement (Lean)
18theorem octaveTrajectory_periodic (amp t : ℝ) :
19 octaveTrajectory amp (t + 2 * Real.pi) = octaveTrajectory amp t := by
proof body
Tactic-mode proof.
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