126 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
127 |
125 |
128 \begin{frame}\frametitle{Fourier Transform 1: Specification} |
126 \begin{frame}\frametitle{Fourier Transform 1: Specification} |
129 {\footnotesize\it |
127 {\footnotesize\it |
130 Fourier Transform |
128 Fourier Transform |
|
129 |
131 \begin{tabbing} |
130 \begin{tabbing} |
132 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
131 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
133 \>given \>:\> Time continiues, not periodic Signal \\ |
132 \>given \>:\> Time continiues, not periodic Signal \\ |
134 \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\ |
133 \> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\ |
135 \>precond \>:\> TODO\\ |
134 \>precond \>:\> TODO\\ |
174 %% Transform expl 2 SPEC %% |
173 %% Transform expl 2 SPEC %% |
175 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
174 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
176 |
175 |
177 \begin{frame}\frametitle{Fourier Transform 2: Specification} |
176 \begin{frame}\frametitle{Fourier Transform 2: Specification} |
178 {\footnotesize\it |
177 {\footnotesize\it |
179 Fourier Transform |
178 |
|
179 \textbf{(a)} Determine the fourier transform for the given rectangular impulse: |
|
180 |
|
181 \begin{center} |
|
182 $x(t)= \left\{ |
|
183 \begin{array}{lr} |
|
184 1 & -1\leq t\geq1\\ |
|
185 0 & else |
|
186 \end{array} |
|
187 \right.$ |
|
188 \end{center} |
|
189 |
180 \begin{tabbing} |
190 \begin{tabbing} |
181 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
191 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
182 \>given \>:\> piecewise\_function \\ |
192 \>given \>:\> piecewise\_function \\ |
183 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\ |
193 \> \> \> \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\ |
184 %?(iterativer) datentyp in Isabelle/HOL |
194 %?(iterativer) datentyp in Isabelle/HOL |
185 \> \> \> translation $T=2$\\ |
195 \> \> \> translation $T=2$\\ |
186 %WN these 2 inputs calculated to [(0,-\infty<t<-1), (1,-1\leq t\leq 1), (0, 1<t<\infty)] |
|
187 %WN translation helpful only, if solution available from other calculation - DROP T ??? |
|
188 \>precond \>:\> TODO\\ |
196 \>precond \>:\> TODO\\ |
189 \>find \>:\> $X(j\cdot\omega)$\\ |
197 \>find \>:\> $X(j\cdot\omega)$\\ |
190 \>postcond \>:\> TODO\\ |
198 \>postcond \>:\> TODO\\ |
191 \end{tabbing} |
199 \end{tabbing} |
192 |
200 |
195 |
203 |
196 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
197 %% Transform expl 2 CALC %% |
205 %% Transform expl 2 CALC %% |
198 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
199 |
207 |
200 \begin{frame}\frametitle{Fourier Transform 2: Calculation} |
208 %\begin{frame}\frametitle{Fourier Transform 2: Calculation} |
201 \footnotesize{ |
209 %\footnotesize{ |
202 \begin{tabbing} |
210 %\begin{tabbing} |
203 000\=\kill |
211 %000\=\kill |
204 %WN first |
212 %01 \> ${\cal F}\;(x(t-2)) =$\\ |
205 01 \> ${\cal F}\;(x(t-2)) =$\\ |
213 % \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\ |
206 \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\ |
214 %02 \> $e^{-j\cdot\omega\cdot 2}\cdot X\;(j\cdot\omega)$\\ |
207 02 \> $e^{-j\cdot\omega\cdot 2}\cdot X\;(j\cdot\omega)$\\ |
215 % \`definition $X\;(j\cdot\omega)$\\ |
208 \`definition $X\;(j\cdot\omega)$\\ |
216 %03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\ |
209 03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\ |
217 % \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\ |
210 \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\ |
218 %04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\ |
211 04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\ |
219 % \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\ |
212 \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\ |
220 %05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\ |
213 05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\ |
221 % %\` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\ |
214 %\` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\ |
222 % \` pbl: integration in $\cal C$\\ |
215 \` pbl: integration in $\cal C$\\ |
223 %06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\ |
216 06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\ |
224 % \` $f\;t\;|_a^b = f\;b-f\;a$\\ |
217 \` $f\;t\;|_a^b = f\;b-f\;a$\\ |
225 %07 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 1} - \frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot -1})$\\ |
218 07 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot 1} - \frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot -1})$\\ |
226 %\vdots\` pbl: simplification+factorization in $\cal C$\\ |
219 \vdots\` pbl: simplification+factorization in $\cal C$\\ |
227 %08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\ |
220 08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\ |
228 % \` trick~!\\ |
221 \` trick~!\\ |
229 %09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\ |
222 09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\ |
230 % \` table\\ |
223 \` table\\ |
231 %10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$ |
224 10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$ |
232 %\end{tabbing} |
225 \end{tabbing} |
233 %} |
226 } |
234 %\end{frame} |
227 \end{frame} |
|
228 |
235 |
229 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
236 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
230 %% Transform expl 2 REQ %% |
237 %% Transform expl 2 REQ %% |
231 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
238 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
232 |
239 |
233 %WN ... |
|
234 \begin{frame}\frametitle{Fourier Transform 2: Development effort} |
240 \begin{frame}\frametitle{Fourier Transform 2: Development effort} |
235 {\small |
241 {\small |
236 \begin{center} |
242 \begin{center} |
237 \begin{tabular}{l|l|r} |
243 \begin{tabular}{l|l|r} |
238 requirements & comments &effort\\ \hline\hline |
244 requirements & comments &effort\\ \hline\hline |
273 %% DTS SPEC %% |
279 %% DTS SPEC %% |
274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
275 |
281 |
276 \begin{frame}\frametitle{Convolution: Specification} |
282 \begin{frame}\frametitle{Convolution: Specification} |
277 {\footnotesize\it |
283 {\footnotesize\it |
278 Convolution |
284 |
|
285 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response: |
|
286 |
|
287 \begin{center} |
|
288 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\ |
|
289 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$ |
|
290 \end{center} |
|
291 |
|
292 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. |
|
293 |
279 \begin{tabbing} |
294 \begin{tabbing} |
280 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
295 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
281 \>given \>:\> Signals h1[n], h2[n] \\ |
296 \>given \>:\> Signals h1[n], h2[n] \\ |
282 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\ |
297 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\ |
283 %?(iterativer) datentyp in Isabelle/HOL |
298 %?(iterativer) datentyp in Isabelle/HOL |
347 %% Z-Transform SPEC %% |
362 %% Z-Transform SPEC %% |
348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
349 |
364 |
350 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Specification} |
365 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Specification} |
351 {\footnotesize\it |
366 {\footnotesize\it |
352 Convolution |
367 |
|
368 Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion. |
|
369 |
|
370 \begin{center} |
|
371 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable |
|
372 \end{center} |
|
373 |
353 \begin{tabbing} |
374 \begin{tabbing} |
354 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
375 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
355 \>given \>:\> Expression of z \\ |
376 \>given \>:\> Expression of z \\ |
356 \> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\ |
377 \> \> \> \>(X (z::real\,+z::imag),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\ |
357 \>precond \>:\> TODO\\ |
378 \>precond \>:\> TODO\\ |