Iterated derivatives of x ↦ c cos(a x₀)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.iteratedDeriv_cos_mul (a c : ℝ) (k : ℕ) : (iteratedDeriv k fun (s : ℝ) => c * Real.cos (a * s)) = fun (s : ℝ) => c * a ^ k * Real.cos (a * s + ↑k * (Real.pi / 2))

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.contDiff_cosDatum (c a : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => c * Real.cos (a * x 0)

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.iteratedFDeriv_cosDatum (c a : ℝ) (k : ℕ) (x : Homogenization.Vec 2) (m : Fin k → Homogenization.Vec 2) : (iteratedFDeriv ℝ k (fun (x : Homogenization.Vec 2) => c * Real.cos (a * x 0)) x) m = (∏ j : Fin k, m j 0) * (c * a ^ k * Real.cos (a * x 0 + ↑k * (Real.pi / 2)))

theorem AVenhance.Infra.FullTheorem.NoSelectionInputs.prod_basisVec_zero {k : ℕ} (i : Fin k → Fin 2) : ∏ j : Fin k, Homogenization.basisVec (i j) 0 = if ∀ (j : Fin k), i j = 0 then 1 else 0