% (find-LATEX "2024-1-C3-tipos.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2024-1-C3-tipos.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2024-1-C3-tipos.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2024-1-C3-tipos.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2024-1-C3-tipos.pdf"))
% (defun e () (interactive) (find-LATEX "2024-1-C3-tipos.tex"))
% (defun o () (interactive) (find-LATEX "2023-2-C3-tipos.tex"))
% (defun u () (interactive) (find-latex-upload-links "2024-1-C3-tipos"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2024-1-C3-tipos.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
%          (code-eec-LATEX "2024-1-C3-tipos")
% (find-pdf-page   "~/LATEX/2024-1-C3-tipos.pdf")
% (find-sh0 "cp -v  ~/LATEX/2024-1-C3-tipos.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2024-1-C3-tipos.pdf /tmp/pen/")
%     (find-xournalpp "/tmp/2024-1-C3-tipos.pdf")
%   file:///home/edrx/LATEX/2024-1-C3-tipos.pdf
%               file:///tmp/2024-1-C3-tipos.pdf
%           file:///tmp/pen/2024-1-C3-tipos.pdf
%  http://anggtwu.net/LATEX/2024-1-C3-tipos.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-cps   "Caepro5 Piecewise2 Maxima2")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2")
% (find-MM-aula-links "2024-1-C3-tipos" "3" "c3m241tipos" "c3ti")

% «.defs»		(to "defs")
% «.defs-T-and-B»	(to "defs-T-and-B")
% «.defs-caepro»	(to "defs-caepro")
% «.defs-pict2e»	(to "defs-pict2e")
% «.defs-maxima»	(to "defs-maxima")
% «.title»		(to "title")
% «.links»		(to "links")



\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb}                  % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
%\usepackage{proof}   % For derivation trees ("%:" lines)
%\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
            top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
           ]{geometry}
%
\begin{document}

% «defs»  (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")

\def\drafturl{http://anggtwu.net/LATEX/2024-1-C3.pdf}
\def\drafturl{http://anggtwu.net/2024.1-C3.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}

% (find-LATEX "2024-1-C2-carro.tex" "defs-caepro")
% (find-LATEX "2024-1-C2-carro.tex" "defs-pict2e")

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% «defs-T-and-B»  (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B       (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}

% «defs-caepro»  (to ".defs-caepro")
%L dofile "Caepro5.lua"              -- (find-angg "LUA/Caepro5.lua" "LaTeX")
\def\Caurl   #1{\expr{Caurl("#1")}}
\def\Cahref#1#2{\href{\Caurl{#1}}{#2}}
\def\Ca      #1{\Cahref{#1}{#1}}

% «defs-pict2e»  (to ".defs-pict2e")
%L dofile "Piecewise2.lua"           -- (find-LATEX "Piecewise2.lua")
%L --dofile "Escadas1.lua"           -- (find-LATEX "Escadas1.lua")
\def\pictgridstyle{\color{GrayPale}\linethickness{0.3pt}}
\def\pictaxesstyle{\linethickness{0.5pt}}
\def\pictnaxesstyle{\color{GrayPale}\linethickness{0.5pt}}
\celllower=2.5pt

% «defs-maxima»  (to ".defs-maxima")
%L dofile "Maxima2.lua"              -- (find-angg "LUA/Maxima2.lua")
\pu

\def\rq{\ColorRed{?}}
\def\undq#1{\underbrace{#1}_{\rq}}

% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\co#1{{%
  \def\"{\char34}%
  \def\%{\char37}%
  \def\\{\char92}%
  \def\^{\char94}%
  \def\~{\char126}%
  \tt#1%
  }}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}




%  _____ _ _   _                               
% |_   _(_) |_| | ___   _ __   __ _  __ _  ___ 
%   | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
%   | | | | |_| |  __/ | |_) | (_| | (_| |  __/
%   |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
%                      |_|          |___/      
%
% «title»  (to ".title")
% (c3m241tiposp 1 "title")
% (c3m241tiposa   "title")

\thispagestyle{empty}

\begin{center}

\vspace*{1.2cm}

{\bf \Large Cálculo 3 - 2024.1}

\bsk

Aula 6: tipos e limites

\bsk

Eduardo Ochs - RCN/PURO/UFF

\url{http://anggtwu.net/2024.1-C3.html}

\end{center}

\newpage

% «links»  (to ".links")
% (c3m241tiposp 2 "links")
% (c3m241tiposa   "links")

{\bf Links}

\scalebox{0.6}{\def\colwidth{14cm}\firstcol{

% (find-books "__analysis/__analysis.el" "bortolossi")
% (find-books "__analysis/__analysis.el" "bortolossi" "164" "Fig. 5.1: Interpretação geométrica")

\par \Ca{Bort5p2} (p.164) Fig. 5.1: Interpretação geométrica da derivada
\par \Ca{StewPtCap10} Cap.10: Equações Paramétricas e Coordenadas Polares

% (find-books "__analysis/__analysis.el" "stewart-pt")
% (find-books "__analysis/__analysis.el" "stewart-pt" "575" "10 Equações Paramétricas")
% (find-stewart72ptpage (+ -489  575) "10 Equações Paramétricas e Coordenadas Polares")
% (find-stewart72pttext (+ -489  575))


}\anothercol{
}}

\newpage

\newpage

% «C»  (to ".C")
% (c3m232tiposp 3 "C")
% (c3m232tiposa   "C")
% (c3m222typesp 2 "C")
% (c3m222typesa   "C")

{\bf C}

\def\und#1#2{\underbrace{#1}_{#2}}
\def\printfcomtipos#1#2#3#4#5{
  \und{
  \co{printf(}
  \und{\co{\"\%f\"}}{\co{#1}}
  \co{,\ }
  \und{\und{\co{c}}{\co{#2}}
       \co{+}
       \und{\co{a}}{\co{#3}}
      }{\co{#4}}
  \co{)}
  }{\co{#5}}
  }


\scalebox{0.8}{\def\colwidth{8cm}\firstcol{

    Em $\tt C$ cada subexpressão retorna um valor, e cada valor tem um
    tipo. Por exemplo, depois destas declarações
    % 
    $$\begin{tabular}{l}
        \co{char c = 100;} \\
        \co{float a = 2.34;} \\
      \end{tabular}
    $$

    Temos os dois diagramas à direita. Repare que o primeiro diz o
    tipo de cada subexpressão e o segundo diz o valor, ou o resultado,
    daquela subexpressão.

    \ssk

    Esses dois diagramas {\sl se complementam}. A maioria dos
    exercícios deste PDF vai pedir que você faça o diagrama de tipos,
    e alguns deles vão ter sugestões tipo ``se você estiver
    completamente perdido considere o caso particular tal e faça o
    diagrama de valores dele... e depois tente fazer o diagrama de
    tipos''.

}\anothercol{

$\printfcomtipos{char\ *}{char}{float}{float}{int}$

\bsk

$\printfcomtipos{\"\%f\"}{100}{2.34}{102.34}{6}$

}}


\newpage

% «funcoes»  (to ".funcoes")
% (c3m232tiposp 4 "funcoes")
% (c3m232tiposa   "funcoes")
% (c3m232tiposp 4 "funcoes")
% (c3m232tiposa   "funcoes")

{\bf Funções}


\scalebox{0.7}{\def\colwidth{8cm}\firstcol{

    Em {\tt C} o ``valor'' do \co{printf} é um número de 64 bits --- o
    endereço do código da função \co{printf} --- com um tipo
    complicado... quando eu rodei o GDB no programa da página anterior
    e perguntei pra ele o tipo e o valor do \co{printf} ele respondeu isso aqui:
    % 
    $$
    \begin{tabular}{l}
      \co{(gdb)\ p\ printf} \\
      \co{\$1\ =\ \{int\ (const\ char\ *,\ ...)\}} \\
      \co{\ \ \ \ \ \ \ 0x7ffff7e3bcf0\ <\_\_printf>} \\
      \co{(gdb)} \\
    \end{tabular}
    $$

    Livros de Matemática geralmente consideram que funções são
    conjuntos. Por exemplo, se
    %
    $$\begin{array}{rcrcl}
      f &:& \R &\to & \R \\
         &&  x &\mto& x^2 \\
      \end{array}
    $$

}\anothercol{

    então $f$ --- ou: o ``valor'' de $f$ --- é o gráfico da função
    $f$, que é uma párabola em $\R^2$, e é um subconjunto de $\R^2$
    contendo infinitos pontos... ou seja: nesse caso o valor de $f(3)$
    é 9, que é um número, mas o ``valor'' de $f$ é um conjunto
    infinito!!! \standout{Cuidado!} $\frown$

    \msk

    {\sl Dica:} leia as páginas 31--33 do capítulo 1 do Leithold pra
    ver como ele define funções. A gente só vai entender {\sl direito}
    o conceito de ``variável dependente'', que ele menciona na página
    32, quando a gente começar a entender ``notação de físicos'',
    daqui a algumas aulas... pra resumir {\sl muito}: ``variáveis
    dependentes'' existem em ``notação de físicos'' e não existem em
    ``notação de matemáticos'', e a gente vai ver como traduzir entre
    as duas notações.

}}


% (find-man "3 sqrt")

\newpage


% «tipos»  (to ".tipos")
% (c3m232tiposp 5 "tipos")
% (c3m232tiposa   "tipos")
% (c3m222typesp 3 "tipos")
% (c3m222typesa   "tipos")
% (c3m212typesp 2 "tipos")
% (c3m212typesa   "tipos")
% (c3m211vlp 3 "tipos")
% (c3m211vla   "tipos")
% (find-LATEXgrep "grep --color=auto -nH --null -e tipos 2020-2-C3*.tex")
% (c3m202rcadeia1p 8 "tipos")
% (c3m202rcadeia1a   "tipos")

{\bf Tipos}

\ssk

\scalebox{0.6}{\def\colwidth{8.5cm}\firstcol{

{\bf TUDO} que nós vamos fazer em Cálculo 3 pode ser {\sl visualizado}
e {\sl tipado}. Você já viu um pouco de tipos em {\tt C} e em Física;
em Física os ``tipos'' são parcialmente determinados pelas unidades
--- metros são distância, segundos são tempo, metros/segundo é uma
unidade de velocidade, e assim por diante... em {\tt C} um {\tt char},
um {\tt int}, um {\tt float} e um {\tt (void *)} são coisas bem
diferentes.

\ssk

Obs: o jeito como nós vamos usar tipos em Cálculo 3 vai ser bastante
improvisado. Se você googlar por ``Type Theory'' você vai encontrar
montes de referências a teorias de tipos que podem ser totalmente
formalizadas, mas os tipos que nós vamos usar em C3 são muito mais
``intuitivos'' do que ``formais''.

\ssk
}\anothercol{

% (find-bortolossi5page (+ -162 164) "5.2. Definições e exemplos")
% (find-bortolossi5page (+ -162 165)   "Fig. 5.2: Interpretação geométrica")

Dê uma olhada nas páginas 164 a 166 do capítulo 5 do Bortolossi:

\ssk

\Ca{Bort5p2} (p.164) 5.2 Definições e exemplos

\ssk

Todas as expressões que aparecem lá podem ser ``tipadas'' e
interpretadas como posições no eixo $x$ (ou no eixo $y$, ou no eixo
$y$), ou como distâncias no eixo $x$ (ou no eixo $y$, ou $z$), ou como
{\sl inclinações}... vamos ver os detalhes disto aos poucos.

\ssk

Nos próximos exercícios você vai tentar ``tipar'' cada subexpressão
deles. Escreva os seus tipos nos lugares em que eu pus as `$\rq$'s.
Use português, improvise o quanto precisar, invente abreviações -- mas
tente encontrar as melhores abreviações possíveis -- e compare o seu
modo de escrever os tipos com os dos seus colegas. Lembre que aqui nós
estamos tentando fazer explicitamente, num diagrama, algo que os
livros fazem em poucas frases de texto fingindo que é algo óbvio.

Se você tiver dificuldade de fazer o caso geral faça um caso
particular primeiro.


}}

\newpage

% «exercicio-1»  (to ".exercicio-1")
% (c3m232tiposp 6 "exercicio-1")
% (c3m232tiposa   "exercicio-1")
% (c3m222typesp 5 "exercicio-1")
% (c3m222typesa   "exercicio-1")
% (c3m212typesp 3 "exercicio-1")
% (c3m212typesa   "exercicio-1")
% (c3m211vlp 5 "exercicio-1")
% (c3m211vla   "exercicio-1")
% (c3m202rcadeia1p 32 "tipos-de-novo")
% (c3m202rcadeia1a    "tipos-de-novo")

{\bf Exercício 1}

Digamos que $f(x)=x^2$ e que $y=f(x)$. 

Se você tiver dificuldade de pensar no caso geral

faça $x_0=1$ e $Δx=0.1$.

$$\undq{
  \undq{(\undq{\undq{f}(\undq{\undq{x_0} + \undq{Δx}})}
        - \undq{\undq{f}(\undq{x_0})})} / \undq{Δx}
  }
$$


\newpage

% «exercicio-2»  (to ".exercicio-2")
% (c3m232tiposp 7 "exercicio-2")
% (c3m232tiposa   "exercicio-2")
% (c3m212typesp 4 "exercicio-2")
% (c3m212typesa   "exercicio-2")
% (c3m211vlp 6 "exercicio-2")
% (c3m211vla   "exercicio-2")

{\bf Exercício 2}

Digamos que $f(t)=\cos t$, $g(t)=\sen t$, e $P(t)=(f(t),g(t))$. 

Se você tiver dificuldade de pensar no caso geral

faça $t_0=\fracπ2$ e $Δt=0.1$.

$$\undq{
  \undq{(\undq{\undq{P}(\undq{\undq{t_0} + \undq{Δt}})}
        - \undq{\undq{P}(\undq{t_0})})} / \undq{Δt}
  }
$$

\newpage

% «exercicio-3»  (to ".exercicio-3")
% (c3m232tiposp 8 "exercicio-3")
% (c3m232tiposa   "exercicio-3")
% (c3m212typesp 5 "exercicio-3")
% (c3m212typesa   "exercicio-3")
% (c3m211vlp 7 "exercicio-3")
% (c3m211vla   "exercicio-3")

{\bf Exercício 3}

Digamos que $f(t)=\cos t$, $g(t)=\sen t$, e $P(t)=(f(t),g(t))$. 

Se você tiver dificuldade de pensar no caso geral

faça $t_0=\fracπ2$ e $Δt=0.1$.
%
$$\undq{\undq{P}(\undq{\undq{t_0} + \undq{Δt}})}
  =
  \undq{
    ( \undq{\undq{f}(\undq{\undq{t_0} + \undq{Δt}})},
      \undq{\undq{g}(\undq{\undq{t_0} + \undq{Δt}})} )
  }
$$

\newpage

% «exercicio-4»  (to ".exercicio-4")
% (c3m232tiposp 9 "exercicio-4")
% (c3m232tiposa   "exercicio-4")
% (c3m212typesp 6 "exercicio-4")
% (c3m212typesa   "exercicio-4")
% (c3m211vlp 8 "exercicio-4")
% (c3m211vla   "exercicio-4")
% (find-bortolossi6page (+ -186 197) "6.2 O vetor tangente a uma curva parametrizada")
% (find-bortolossi6page (+ -186 198)   "mas este vetor limite pode ser calculado")
% (find-bortolossi6page (+ -186 199)   "limite de vetores secantes")

Agora nós vamos começar a ver como decifrar definições

como a das páginas 197--198 do capítulo 6 do Bortolossi:

\msk

\Ca{Bort6p11} (p.197) 6.2 O vetor tangente a uma curva parametrizada

\msk

Ele faz tudo de um jeito bem geral, e ele usa $\R^m$ ao invés

de $\R^2$ ou $\R^3$.

\bsk

{\bf Exercício 4}

Reescreva a conta grande no meio da página 198 do Bortolossi

substituindo $t_0$ por $\fracπ2$, $h_j$ por $ε$,
$x_1(t)$ por $\cos t$, $x_2(t)$ por $\sen t$,

e $m$ por 2. Obs: os `$\ldots$' vão sumir.

\newpage

% «fig-bortolossi»  (to ".fig-bortolossi")
% (c3m232tiposp 10 "fig-bortolossi")
% (c3m232tiposa    "fig-bortolossi")

\scalebox{0.9}{\def\colwidth{12cm}\firstcol{

O livro do Bortolossi tem essa figura daqui na página 199:

\Ca{Bort6p13} (p.199) Figura 6.8: o vetor tangente...

\msk

%
% (find-latexscan-links "C3" "20210625_bortolossi_p199")
% (find-xpdf-page "~/LATEX/2021-1-C3/20210625_bortolossi_p199.pdf")
$$\includegraphics[height=4.5cm]{2021-1-C3/20210625_bortolossi_p199.pdf}$$

Isso é um desenho de vetor velocidade como limite de retas secantes
num caso geral -- o Bortolossi não nos diz quem são $α:\R→\R^2$, nem
$t_0$, nem a sequência $(h_1, h_2, h_3, \ldots)$, e isso sugere que
essa figura vai valer pra quaisquer $α$, $t_0$ e $(h_1, h_2, \ldots)$,
com as devidas adaptações...

}\anothercol{
}}


\newpage

% «exercicio-5»  (to ".exercicio-5")
% (c3m232tiposp 11 "exercicio-5")
% (c3m232tiposa    "exercicio-5")
% (c3m212typesp 8 "exercicio-5")
% (c3m212typesa   "exercicio-5")
% (c3m211vlp 10 "exercicio-5")
% (c3m211vla    "exercicio-5")

{\bf Exercício 5}

Aqui nós vamos tentar fazer uma figura parecida com

a do caso anterior, mas com $α(t) = (\cos t, \sen t)$, $t_0=\fracπ2$,

$h_0 = \fracπ2$, $0 < \ldots < h_3 < h_2 < h_1 < h_0$, $\lim_{j→∞} h_j = 0$.

Comece com esta figura aqui,
%
% (find-latexscan-links "C3" "20210625_bortolossi_p199_hack")
% (find-xpdf-page "~/LATEX/2021-1-C3/20210625_bortolossi_p199_hack.pdf")
$$\includegraphics[height=3cm]{2021-1-C3/20210625_bortolossi_p199_hack.pdf}$$

e encontre valores razoáveis para $h_1$, $h_2$ e $h_3$ que te

permitam completar o desenho no olhômetro fazendo

as contas de cabeça com aproximações bem grosseiras.



\newpage

%  _   _ _____ 
% | \ | |  ___|
% |  \| | |_   
% | |\  |  _|  
% |_| \_|_|    
%              
% «intro-nf»  (to ".intro-nf")
% (c3m232tiposp 12 "intro-nf")
% (c3m232tiposa    "intro-nf")
% (c3m212typesp 9 "intro-nf")
% (c3m212typesa   "intro-nf")

{\bf Introdução à ``notação de físicos''}

\ssk

Nós vamos aprender a usar duas convenções de notação matemática no
curso -- ou, pra encurtar, duas ``notações''. O Bortolossi usa uma
notação muito mais precisa, que eu vou chamar de ``notação de
matemáticos'', e o Silvanus Thompson usa uma notação mais intuitiva
mas bem mais difícil de formalizar, que eu vou chamar de ``notação de
físicos''.

\ssk

Na ``notação de físicos'' muitos símbolos vão ser {\sl abreviações} e
as regras pra expandir essas abreviações vão depender do contexto. Vão
existir algumas convenções pra expandir essas abreviações que vão ser
seguidas {\sl quase} sempre, mas vão existir muitas exceções -- e
muitos casos ambíguos...

\newpage

% «primeiro-exemplo»  (to ".primeiro-exemplo")
% (c3m232tiposp 13 "primeiro-exemplo")
% (c3m232tiposa    "primeiro-exemplo")
% (c3m212typesp 10 "primeiro-exemplo")
% (c3m212typesa    "primeiro-exemplo")
% (c3m211nfp 6 "primeiro-exemplo")
% (c3m211nfa   "primeiro-exemplo")

{\bf Um primeiro exemplo}

Digamos que $y=\sqrt{x}$.

Podemos considerar que $x$ e $y$ ``variam juntos'',

``obedecendo certas restrições''. O conjunto dos pontos $(x,y)$

que obedecem essas restrições é $\setofxyst{y = \sqrt{x}}$

e o gráfico é:
%
% (find-latexscan-links "C3" "20210804_sqrt")
% (find-xpdf-page "~/LATEX/2021-1-C3/20210804_sqrt.pdf")
$$\myvcenter{\includegraphics[height=4cm]{2021-1-C3/20210804_sqrt.pdf}}
  \qquad
  \begin{array}{rcl}
    x_0,x_1&∈&\R \\ 
    y_0 &=& \sqrt{x_0} \\ 
    y_1 &=& \sqrt{x_1} \\ 
    Δx &=& x_1 - x_0 \\
    Δy &=& y_1 - y_0 \\
    \\
  \end{array}
$$



\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}



% Local Variables:
% coding: utf-8-unix
% ee-tla: "c3ti"
% ee-tla: "c3m241tipos"
% End:
