doc-src/isac/jrocnik/present-1.tex
branchdecompose-isar
changeset 42076 6d1a17840fc8
parent 42075 7d062ed7359c
child 42122 cc5daace30bb
child 42149 87fd7d13e814
equal deleted inserted replaced
42075:7d062ed7359c 42076:6d1a17840fc8
   137 \begin{frame}\frametitle{TODO}
   137 \begin{frame}\frametitle{TODO}
   138 TODO
   138 TODO
   139 \end{frame}
   139 \end{frame}
   140 
   140 
   141 \subsection[Transform]{Fourier transform}
   141 \subsection[Transform]{Fourier transform}
   142 \begin{frame}\frametitle{Fourier transform expl 1}
   142 \begin{frame}\frametitle{FT expl 1}
   143 TODO
   143 TODO
   144 \end{frame}
   144 \end{frame}
   145 
   145 
   146 \begin{frame}\frametitle{Fourier transform expl 2a}
   146 \begin{frame}\frametitle{FT expl 2a}
   147 TODO
   147 TODO
   148 \end{frame}
   148 \end{frame}
   149 
   149 
   150 \begin{frame}\frametitle{Fourier transform expl 2b}
   150 \begin{frame}\frametitle{FT expl 2b}
   151 Aufgabenstellung von Bernhard
   151 Problem (from Bernhard)
   152 \end{frame}
   152 \end{frame}
   153 
   153 
   154 \begin{frame}\frametitle{Fourier transform expl 2b}
   154 \begin{frame}\frametitle{FT expl 2b: specification }
       
   155 {\footnotesize\it
       
   156 fourier transform
       
   157 \begin{tabbing}
       
   158 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
       
   159 \>given    \>:\>  piecewise\_function \\
       
   160 \>         \> \>  \>$(x (t::real), [(0,-\infty<t<1), (1,1\leq t\leq 3), (0, 3<t<\infty)])$\\
       
   161                         %?(iterativer) datentyp in Isabelle/HOL
       
   162 \>         \> \>  translation $T=2$\\
       
   163 \>precond  \>:\>  TODO\\
       
   164 \>find     \>:\>  $X(j\cdot\omega)$\\
       
   165 \>postcond \>:\>  TODO\\
       
   166 \end{tabbing}
       
   167 
       
   168 }
       
   169 \end{frame}
       
   170 
       
   171 \begin{frame}\frametitle{FT expl 2b: calculation}
   155 \footnotesize{
   172 \footnotesize{
   156 \begin{tabbing}
   173 \begin{tabbing}
   157 000\=\kill
   174 000\=\kill
   158 01 \> ${\cal F}\;(x(t-2)) =$\\
   175 01 \> ${\cal F}\;(x(t-2)) =$\\
   159       \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\
   176       \`${\cal F}\;(x(t-T)) = e^{-j\cdot\omega\cdot T}\cdot X\;j\cdot\omega$\\
   162 03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\
   179 03 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-\infty}^\infty x\;t\;\cdot e^{-j\cdot\omega\cdot t} d t$\\
   163       \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\
   180       \` $x\;t = 1\;{\it for}\;\{x.\;-1\leq t\;\land\;t\leq 1\}\;{\it and}\;x\;t=0\;{\it otherwise}$\\
   164 04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\
   181 04 \> $e^{-j\cdot\omega\cdot 2}\cdot \int_{-1}^1 1\cdot e^{-j\cdot\omega\cdot t} d t$\\
   165       \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\
   182       \` $\int_a^b f\;t\;dt = \int f\;t\;dt\;|_a^b$\\
   166 05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\
   183 05 \> $e^{-j\cdot\omega\cdot 2}\cdot \int 1\cdot e^{-j\cdot\omega\cdot t} d t\;|_{-1}^1$\\
   167       \` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\
   184       %\` $\int e^{a\cdot t} = \frac{1}{a}\cdot e^{a\cdot t}$\\
       
   185        \` pbl: integration in $\cal C$\\
   168 06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\
   186 06 \> $e^{-j\cdot\omega\cdot 2}\cdot (\frac{1}{-j\cdot\omega}\cdot e^{-j\cdot\omega\cdot t} \;|_{-1}^1)$\\
   169       \` $f\;t\;|_a^b = f\;b-f\;a$\\
   187       \` $f\;t\;|_a^b = f\;b-f\;a$\\
   170 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})$\\
   188 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})$\\
   171 \vdots\` simplification+factorization in $\cal C$\\
   189 \vdots\` pbl: simplification+factorization in $\cal C$\\
   172 08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\
   190 08 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{-j\cdot\omega}\cdot(e^{j\cdot\omega} - e^{-j\cdot\omega})$\\
   173       \` trick~!\\
   191       \` trick~!\\
   174 09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\
   192 09 \> $e^{-j\cdot\omega\cdot 2}\cdot \frac{1}{\omega}\cdot(\frac{-e^{j\cdot\omega} + e^{-j\cdot\omega}}{j})$\\
   175       \` table\\
   193       \` table\\
   176 10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$
   194 10 \> $e^{-j\cdot\omega\cdot 2}\cdot 2\cdot\frac{\sin\;\omega}{\omega}$
   177 \end{tabbing}
   195 \end{tabbing}
   178 }
   196 }
   179 \end{frame}
   197 \end{frame}
   180 
   198 
   181 \begin{frame}\frametitle{Fourier transform expl 2b}
   199 \begin{frame}\frametitle{FT expl 2b}
   182 Voraussetzungen
   200 prerequisites
   183 
   201 \end{frame}
   184 
   202 
   185 \end{frame}
   203 \section[Discrete time]{Discrete-time systems}
   186 
   204 \subsection[Convolution]{Convolution}
   187 \begin{frame}\frametitle{Fourier transform expl 2b - table}
       
   188 TODO
       
   189 \end{frame}
       
   190 
       
   191 \section[Convolution]{Convolution}
       
   192 %\subsection[]{}
       
   193 \begin{frame}\frametitle{Convolution (Faltung)}
   205 \begin{frame}\frametitle{Convolution (Faltung)}
   194 TODO
   206 TODO
   195 \end{frame}
   207 \end{frame}
   196 
   208 
   197 \section[${\cal Z}$ transform]{${\cal Z}$ transform}
   209 \section[${\cal Z}$ transform]{${\cal Z}$ transform}
   198 %\subsection[]{}
   210 %\subsection[]{}
       
   211 \begin{frame}\frametitle{TODO}
       
   212 TODO
       
   213 \end{frame}
       
   214 
       
   215 \subsection[]{Indextranformation}
   199 \begin{frame}\frametitle{TODO}
   216 \begin{frame}\frametitle{TODO}
   200 TODO
   217 TODO
   201 \end{frame}
   218 \end{frame}
   202 
   219 
   203 \subsection[Inverse ${\cal Z}$]{Inverse ${\cal Z}$ transform}
   220 \subsection[Inverse ${\cal Z}$]{Inverse ${\cal Z}$ transform}
   223 effort --- in 45min units\\
   240 effort --- in 45min units\\
   224 MT --- thesis ``factorization'' (mathematics)
   241 MT --- thesis ``factorization'' (mathematics)
   225 }
   242 }
   226 \end{frame}
   243 \end{frame}
   227 
   244 
   228 \section[]{Indextranformation}
       
   229 %\subsection[]{}
       
   230 \begin{frame}\frametitle{TODO}
       
   231 TODO
       
   232 \end{frame}
       
   233 
       
   234 
   245 
   235 \end{document}
   246 \end{document}
   236 
   247 
   237 
   248