На основе некоторых нелинейных ограничений на$a_k$,$b_k$Я должен найти выполнимый набор следующего выражения ряда Фурье:

$ x(t)= {a_0+ \sum_{k=1}^{\infty}   (a_k\cos(2\pi f_0 kt)+(b_k\sin(2\pi f_0 kt))}

Принимая во внимание, что ограничения на$a_k$,$b_k$ а также$a_0$ являются

$ L \leq a_0 \leq U $

$ Lower_bound \leq a_k^2+b_k^2 \leq Upper_bound

Могу ли я сделать это с помощью Z3?

В дополнение к этому я могу использовать Z3 для показательных функций, имеющих сложные степени, например в выражении преобразования Фурье.