self study IDMb: Introdução à Demonstração Matemática (teoria dos números reais)

Sessões

Leia bem o FAQ sobre hw. Note também que:

• Homeworks são atribuidos também durante as aulas e no Zulip.
• Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

IDMb (1,2) [video]

• Pythagoreanos e a interpretação de número na grécia antiga
• Os números: naturais, inteiros, racionais, reais
• Θ. O √2 é irracional
• Lemma-chave: x² par ⇒ x par
• A “existência” do √2, pelo teorema pythagoreano
• E quem se importa sobre a racionalidade do √2?
• Buracos na linha dos racionais
• A linha continua dos reais
• De √2 para √3
• E sobre o √4?
• Tentativa de generalização para outros √n
• Como demonstrar a parte de: «não há outra saida»
• Especificação dos reais (1/3): parte algébrica (aditiva e multiplicativa)
• O que podemos aproveitar «de graça» dos teoremas da teoria dos números inteiros?
• Uma divulgação/propaganda de álgebra abstrata
• Especificação dos reais (2/3): parte relacional (ordem)
• Definições usando as noções primitivas da especificação, e qual o trabalho dum implementador
• Notação: a⁻¹ e a/b; o uso do artigo definido, e a necessidade de demonstrar existência e unicidade
• A unicidade da identidade aditiva: o que significa
• Definições dos a⁻¹ e a/b
• O que precisamos demonstrar sobre nossas novas noções definidas
• potências de um real elavado a um natural
• potências de um real elavado a um inteiro
• potências de um real elavado a um racional
• potências de um real elavado a um real: impossível conseguir isso ainda

hw

1. ³√2 é irracional? ³√3? ᵏ√n?
2. §«Primeiros passos»
3. §«Ordem e positividade»
4. §«Subconjuntos notáveis e inaceitáveis»
5. (IDMa) Para quais naturais n temos mesmo que (∀x : Int)[n | x² ⇒ n | x]?

IDMb (3,4) [video]

• Θ. cancelamento aditivo pela esquerda (RA-CanL)
• Θ. resoluções únicas
• duas maneiras diferentes de escrever uma demonstração
• como justificar o “somar o mesmo real nos dois lados”
• funções anônimas, notação lambda, notação “mapsto” (↦)
• umas demonstrações dos primeiros teoremas sobre reais
• valor absoluto nos reais: definição e sua interpretação geométrica
• distância: especificação e implementação
• a desigualdade triangular e sua interpretação geométrica
• demonstração de (∀a,b,c)[ |a - c| ≤ |a - b| + |b - c| ]
• subconjuntos notáveis de reais; type coercing e type casting

hw

1. Até o «§. Valor absoluto»

IDMb (5,6) [video]

• conjuntos: o que significa em saber qual é um conjunto
• como definir operações entre conjuntos
• como generalizar as operações binárias ∪,∩ para serem aplicáveis em coleções de conjuntos
  • ⋃,⋂ : Set(Set(α)) → Set(α)
  • ⋃,⋂ : Seq(Set(α)) → Set(α)
• as relações (⊆) e (⊇)
• distância e espaços métricos: especificação vs implementações
• Frases legais do ♡:
  • ε-perto
  • ε-vizinhança, ε-bola (aberta/fechada)
• Seqüências: notação e interface e type coercion
• notação sobre intervalos e seqüências
• cota inferior/superior de conjunto, e notação sobrecarregada dos (≤) e (<)
• Igualdades que não são igualdades
• Unicidade de mínima/máxima
• intervalos abertos e fechados e notações que envolvem os -∞/+∞

hw

1. Resolva tudo até o §«Mínima e Máxima»

mais hw

1. Na última aula percebemos que Either não tinha sequer chances de se candidatar para virar um Functor, pois Either não é um Type → Type (mas sim um Type → Type → Type. Mesmo assim, conseguimos verificar que aplicando parcialmente o Either num tipo ε só, chegamos mesmo no Either ε que é mesmo um Type → Type, e logo tem chances de ser um Functor, e descubrimos qual seria a fmap certa pra isso (demonstre se não demonstrou—o que é pra demonstrar mesmo??). Aqui mais duas coisinhas que estão também Type → Type → Type: o próprio (→) e o (×). Investigue para cada um deles, e para cada aplicação parcial dele, se pode ser munida com um fmap para conseguir ser um Functor:
   1. (δ →) : Type → Type
   2. (→ γ) : Type → Type
   3. (α ×) : Type → Type
   4. (× β) : Type → Type

IDMb (7,8) [video]

• seqüências são cidadãos da primeira classe
• cota superior/inferor dum conjunto
• infimum/supremum dum conjunto
• coerção de tipo
• duas maneiras de desenhar seqüências: uma 1-dimensional e uma 2-dimensional
• dando significado para 1 + (aₙ)ₙ e para o (aₙ)ₙ + (bₙ)ₙ
• como definir mesmo uma seqüência que desejamos
• seqüência limitada superiormente/inferiormente
• investigação: a (aₙ)ₙ é cotada?
• seqüência (estritamente) crescente/decrescente
• crescente não implica não-cotada-superiormente
• como demonstrar que uma alegada cota inferior é realmente uma cota inferior
• Conexões com IRI: listas, Empty, Unit, habitantes de α como habitantes do Unit → α
• a melhor cota inferior e a melhor cota superior
• unicidade de supremum e de infimum
• conjuntos sem sup/inf, e sup/inf do ℝ e do Ø
• um mal-entendido comum sobre demonstrações por vacuidade e propriedades dos membros do Ø
• Esboço para definir o conjunto dos reais-naturais
  • Def: conjunto naturalmente indutivo
  • o «melhor» naturalmente indutivo significa o «menor», e «menor» significa «(⊆)-menor»
  • top-down: seja ℐ a coleção de todos os conjuntos indutivos, e considere sua interseção
  • uns não-exemplos de indutivos
  • definição dos reais-naturais $\mathbb R_{\mathbb N}$
  • o que demonstrar sobre o $\mathbb R_{\mathbb N}$
• Plicker: infA ≤ supA ?

hw

1. Resolva tudo até o §«Infimum e supremum»
2. Formulem bem o critério-Davi sobre infimum/supremum (usando epsilons ♡), e demonstrem
3. Demonstre a unicidade de infima/suprema
4. (IRI) Tendo um tipo Real, defina um data type XReal para representar os reais extendidos.
5. Enuncie e demonstre o teorema da indução para os reais-naturais.
6. Ache alguma propriedade que é satisfeita no $\mathbb R_{\mathbb Q}$ mas não no $\mathbb R$. Cuidado: a resposta “óbvia” é errada.

IDMb (9) [video]

• (–)ₙ é um ligador da variável n no escopo de –
• Novamente sobre conjuntos:
  • o que preciso fazer para definir/determinar um conjunto
  • o que significa (=) entre conjuntos
  • união e interseção de uma coleção de conjuntos de α
• Seq(Set(Real)) e Seq(Seq(Real))
• Seqüências são cidadãos da primeira classe; pointwise (∗)
• duas maneiras de definir (∗) entre um Real e um Seq(Real)
• união e interseção de uma coleção de conjuntos
• Exemplos de umas seqüências de conjuntos de reais, suas uniões e suas interseções:
  • ( [0,n) )ₙ
  • ( [n,n+1) )ₙ
• Como demonstrar que 1 ∈ ⋂ₙGₙ
• Desenhando os primeiros membros de seqüências de conjuntos de reais
• a união de uma seqüência decrescente ((⊇)-chain).
• Reais naturais vs naturais: type casting e type coercion
• os ⌊–⌋ e ⌈–⌉ (piso e teto)
• uma seqüência de abertos com interseção fechada e o dual: uma seqüência de fechados com união aberta
• Uma seqüência decrescente ((⊇)-chain) de intervalos abertos com interseção intervalo fechado
• Frases legais do ♡:
  • para valores suficientemente grandes de
  • eventualmente
• Seqüência constante: 3 candidatos para definição
• Seqüência eventualmente constante
• Mais umas gírias:
  • «para valores suficientemente grande de»
  • «eventualmente»

hw

1. Defina as $\mathtt{toNat} : \mathbb R_{\mathbb N} \to \mathsf{Nat}$ e $\mathtt{toRealNat} : \mathsf{Nat} \to \mathbb R_{\mathbb N}$; enuncie o que significa que comportam na maneira desejada; demonstre.
2. Seja (Aₙ)ₙ : Seq(α) uma (⊇)-chain. Demonstre que ⋃ₙAₙ = A₀
3. Seja (Aₙ)ₙ : Seq(α) uma (⊆)-chain. Demonstre que ⋂ₙAₙ = A₀
4. Demonstre que não muda nada se a gente trocar o (≥) por (>) e o (≤) por (<) nas definições de «valores-suficientemente-grandes» e de «eventualmente».
5. Na aula cairam na mesa 3 possíveis definições do que significa «(aₙ)ₙ é constante». Investigue se são equivalentes “duas a duas”:
   1. (∃k)(∀n)[ aₙ = k ]
   2. (∀n)(∀m)[ aₙ = aₘ ]
   3. (∀n)[ aₙ = aₙ₊₁ ]

IDMb (10,11) [video]

• “Escolhendo N(ε)’s”
• Tantando ficar implementação-agnósticos
• Q: «para valores suficientemente grandes de» vs «eventualmente»
• cuidado com a comparação com a notação-O (que é abusiva demais)
• (cont.)
• Q: o que significa «a igualdade não é exatmente simétrica»?
• como interpretar “igualdades” como a inf A = sup B.
• giria: «frequentemente»
• sinônimos de inf/sup: glb/lub, meet/join, ∧/∨
• Chegando na definição de limite
• O tipo de «_ tende ao _»
• Um primeiro palpite
• Duas maneiras que uma definição pode ter «erro de tradução» (de cabeça para o papel)
• • Briga contra o primeiro palpite
• Girias que envolvem tempo/futuro com seqüências: «nunca», «sempre»
• Um segundo palpite
• • Briga contra o primeiro palpite
• Terceiro (e último) palpite: usando «para valores suficientemente grandes de»
• Uma maneira que envolve o «eventualmente»
• Q: podemos definir o que significa «_ tende ao +∞» ?
• traduzindo de nível coração com gírias, para um nível low level e explicito
• uma métrica bem diferente nos reais: a métrica discreta
• Quantificadores, complexidade de entendimento, importância de gírias, estratégia vencedora de jogo
• Interpretação dos ∀∃ em termos jogos
• Def: «convergente»
• Θ. constante ⇒ convergente
• Q. A gente não precisou olhar no ε que o jogador ∀ escolheu
• Def: «divergente»
• Θ. eventualmente constante ⇒ convergente
• • copycat strategy em jogos
• • Demonstração
• Umas seqüências divergentes
• Θ. a ( (-1)ⁿ )ₙ não tende a nenhum ℓ (ela é divergente)
• Def: «autoconvergente»
• Θ. Unicidade dos limites
• Plicker: (i) cotada & crescente ⇒ convergente? (ii) autoconvergente ⇒ convergente?

hw

1. Θ. eventualmente constante ⇒ cotada
2. Θ. convergente ⇒ cotada
3. Θ. autoconvergente ⇒ cotada
4. Θ. convergente ⇒ autoconvergente
5. Θ. Comportamento algébrico de limites
   1. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → a + b
   2. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ab
   3. (aₙ)ₙ → a ⇒ (caₙ)ₙ → ca
   4. ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → a/b
6. Alguma das recíprocas das implicações acima é válida?
7. Θ (sanduíche): (aₙ)ₙ → ℓ & (cₙ)ₙ → ℓ & (aₙ)ₙ ≤ (bₙ)ₙ ≤ (cₙ)ₙ ⇒ ??
8. Θ: $\{a_n\}_n \subseteq {\mathbb R}_{\mathbb Z}$ e $(a_n)_n$ convergente ⇒ ??
9. Definição. Seja $(a_n)_n$ uma seqüência de reais. Seja $(n_i)_i$ uma seqüência de naturais estritamente crescente. Chamamos a $(a_{n_i})_i$ uma subseqüência de $(a_n)_n$.
   1. Θ. autoconvergente com subseq convergente ⇒ convergente
10. Depois de resolver os anteriores, tente demonstrar/refutar os:
    1. autoconvergente ⇒ convergente
    2. cotada superiormente & crescente ⇒ convergente

Prova 3.1

IDMb (12,13) [video]

• epsilons e como encontrá-los
• umas perguntas ainda abertas
• recap de uns teoremas demonstrados
  • Θ. convergente ⇒ autoconvergente
  • Θ. autoconvergente ⇒ cotada
• recap de umas proposições não demonstradas
  • ?. crecente & supcotada ⇒ cotada
  • ?. conjunto supcotado ⇒ possui supremum
  • ?. propriedade dos intervalos aninhados
  • ?. autoconvergente ⇒ convergente
  • ?. cotada ⇒ subseq convergente
• a seqüência (log n)ₙ não é autoconvergente
• def: subseqüência
• liminf e limsup
• epsilons e «como encontrá-los»
  • Θ. limₙ (aₙ+bₙ) = limₙ aₙ + limₙ bₙ
  • Θ. limₙ (aₙ·bₙ) = limₙ aₙ · limₙ bₙ
• O último axioma da especificação dos reais: axioma da completude
• Preview de umas conseqüências:
  • Θ. Existência de raizes
  • Θ. Sistema posicional para numerais dos reais
  • Θ. os reais racionais são densos nos reais
  • Θ. os reais irracionais são densos nos reais

hw

1. Resolva sozinho os teoremas seguintes que demonstramos na aula passada:
   1. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ + bₙ)ₙ → ??
   2. (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙbₙ)ₙ → ??
2. …e o resto do Θ. Comportamento algébrico de limites:
   1. (aₙ)ₙ → a ⇒ (caₙ)ₙ → ??
   2. ?? & (bₙ)ₙ → b ⇒ (bₙ⁻¹)ₙ → ??
   3. ?? & (aₙ)ₙ → a & (bₙ)ₙ → b ⇒ (aₙ/bₙ)ₙ → ??
   4. (aₙ)ₙ → a & ?? ⇒ (aₙᵏ)ₙ → ??
3. Θ. conv ⇒ autoconv
4. Θ. autoconv ⇒ cotada
5. C. conv ⇒ cotada
6. Θ. autoconvergente com subseq convergente ⇒ convergente
7. Θ. 0 < ϑ < 1 ⇒ (ϑⁿ)ₙ → ??
8. Θ. Toda seq possui subseq “monótona”
   • Dica 1: Def. Chamamos o natural k de pico para a (aₙ)ₙ sse (∀n≥k)[ aₖ ≥ aₙ ]
   • Dica 2: Separe em casos: Caso (aₙ)ₙ tem quantidade infinita de picos; Caso contrário.
9. «Agora sim!» Demonstre os: Nested Interval Property de Cantor; Monotone Convergence Theorem; Bolzano–Weierstrass Theorem; Cauchy convergence critérion
   1. Θ. (NIP): Teorema dos intervalos aninhados:
      Se (Iₙ)ₙ é uma (⊇)-cadeia de intervalos fechados habitados da forma Iₙ = [aₙ,bₙ],
      então ⋂ₙIₙ habitado.
      Ainda mais: Se (diam(Iₙ))ₙ → 0, então ⋂ₙIₙ é um singleton!
      • Dica 1: a₀ ≤ a₁ ≤ a₂ ≤ ⋯ ≤ b₂ < b₁ ≤ b₀
      • Dica 2: (aₙ)ₙ sup-cotada; (bₙ)ₙ inf-cotada
      • Dica 3: Encontre a≤b tais que ⋂ₙIₙ = [a,b]
   2. Θ. (MC): cotada & “monótona” ⇒ convergente
   3. Θ. (BW): cotada ⇒ conv subseq
   4. Θ. (CC): autoconvergente ⇒ convergente
10. Αρχιμήδης:
    1. Θ. Os reais naturais não são cotados
    2. Θ. (∀ε>0)(∃n)[ 1/n < ε ]
    3. Θ. (∀s≠0)(∃n)[ ns > 1 ]
    4. Θ. (∀ε>0)[ε$\mathbb R_{\mathbb N}$ não é cotado]
    5. Θ. (∀s≠0)(∀b)(∃n)[ b < ns ]
    6. Θ. (∀b)(∀s≠0)(∃n)[ ns > b ]
    7. Q. Há diferença entra as duas últimas? Como chamarias cada uma no «nível coração»?
11. Existência de raizes
    1. Θ. Raizes de pequenos: a < 1 ⇒ (aₙ)ₙ → √a, onde: $$\begin{align*} a_0 &= 0 \\ a_{n+1} &= a_n + \frac 1 2 (a - a_n^2) \end{align*}$$
       • Dica 1: cotada…
       • Dica 2: …crescente…
       • Dica 3: …logo conv. O que falta agora?
    2. Θ. «Ἵππασος precisa morrer» (aka: «√2 é real»)
       • Dica 1: Considere o H ≝ { x | x² < 2 }
       • Dica 2: Seja h = sup H. Elimine as possibilidades h² < 2 e h² > 2
       • Dica 3: Lembrete: o dado h = sup H é uma conjunção e vamos precisar ambas as suas partes: uma para eliminar o caso h² < 2 e a outra para eliminar o caso h² > 2.
       • Dica 4: Para eliminar caso h² < 2: calcule o (h + 1/n)² para conseguir supcotá-lo por h² + (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «cota superior».
       • Dica 5: Para eliminar caso h² > 2: calcule o (h - 1/n)² para conseguir infcotá-lo por h² - (algo controlavelmente pequeno), e logo por 2, contradizendo a parte de «melhor».
    3. Θ. Existência das raizes ²√
    4. Θ. Existência das raizes ᵏ√
12. Densidades:
    1. Θ. dos reais racionais nos reais
    2. Θ. dos reais irracionais nos reais
13. Cardinalidades (1):
    1. Ache seqüência de reais que “ocupa” os reais naturais
    2. Ache seqüência de reais que “ocupa” os reais inteiros
    3. Ache seqüência de reais que “ocupa” os reais racionais
14. Chega sozinho nas definições de liminf / limsup e depois…:
    1. Θ. (aₙ)ₙ → ℓ ⇒ liminfₙ aₙ = ℓ = limsupₙ aₙ
    2. Θ. infₙ aₙ ≤ liminfₙ aₙ ≤ limsupₙ aₙ ≤ supₙ aₙ
    3. Θ. (∀ε>0)(∃K)(∀k≥K)[ liminfₙ aₙ - ε ≤ aₖ ≤ limsupₙ aₙ + ε ]
    4. Θ. x ≥ limsupₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x + ε ]
    5. Θ. x ≤ liminfₙ aₙ ⇔ (∀ε>0)[ temporariamente (aₙ)ₙ > x - ε ]
    6. Θ. x ≤ limsupₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ > x - ε ]
    7. Θ. x ≥ liminfₙ aₙ ⇔ (∀ε>0)[ freqüentemente (aₙ)ₙ < x + ε ]
    8. Θ. liminfₙ aₙ + liminfₙ bₙ ≤ liminfₙ (aₙ+bₙ) ≤ limsupₙ (aₙ+bₙ) ≤ limsupₙ aₙ + limsupₙ bₙ
    9. Q. liminfₙ(pₙ₊₁ - pₙ) = ? onde pₙ é o n-ésimo primo
    10. Q. liminfₙ (sin(n)) = ?
    11. Q. limsupₙ (sin(n)) = ?
15. Algébricos vs Transcedentais
    1. Existem transcedentais?
16. Qualquer conjunto de reais habitado e finito possui mínimo e máximo

IDMb (14,15) [video]

• Construções de conjuntos/tipos numéricos
• Podemos dizer que o ℝ não tem buracos?
• Igualdade para tipos; igualdade para o Seq(α)
• Seqüências com índices diferentes de naturais, seqs implementadas como funções
• lembrete: teoremas sobre o lado algébrico de limites
• o que significam igualdades que envolvem lim.
• duas notações de operadores aplicados em seqüências
• diagramas comutativos e o teorema de limites algébricos
• Dado um tipo A, o que seriam os tipos A², Aⁿ, A⁰?
• Axioma da completude dos reais: nível-♡
• Θ. sobre inf-cotada ⇒ possui ínfimo?
• Θ. Propriedades arquimedeanas
• Θ. Densidades: dos racionais e dos irracionais nos reais
• Θ. NIP: Nested Interval Property (Cantor); Θ. MCT: Monotone Convergence Theorem
• Sistemas posicionais de numerias para reais: interpretação geométrica (via NIP)
• Θ. Bolzano–Weierstrass: cotada ⇒ possui subseq convergente
• Q: convergente ⇒ todas as subseq convergentes?
• Cauchy
• Θ. 0 < θ < 1 ⇒ (θⁿ)ₙ → 0
• Séries, somatórios parciais: uma maneira de interpretar um «somatório infinito»
• dois exemplos de séries convergentes
• um exemplo de série divergente: a séries harmônica

IDMb (16,17) [video]

• (NIP) ⇒ (BW)
• Um toque de espaços métricos: como definir a diam
• Θ. raizes para reais pequenos
• Θ. √2
• O teorema de rearranjo de Riemann (e um problema com soma telescópica infinita)
• polinômios: algébricos vs transcedentais
• Algébricos vs transcedentais
• Euler, a constante e, Liouville
• Cantor: cobririndo uns subconjuntos de reais com seqüências
• Cantor: primeira demonstração que qualquer seqüência de reais
• Cantor: diagonalização
• Borel, Lebesgue, Kolmogorov: um toque de teoria da medida: probabilidade de acertar um racional no [0,1] dos reais
• Integral Riemann vs Integral Lebesgue

hw

1. Resolva o hw do IDMb (12,13) que não foi resolvido na aula; re-resolva sozinho o que foi.
2. Termine para cada uma das séries que encontramos o que faltou:
   1. $\sum_{n=1}^\infty \frac 1 {2^n}$
   2. $\sum_{n=1}^\infty \frac 1 {n^2}$
   3. $\sum_{n=1}^\infty \frac 1 n$
3. O conjunto dos irracionais é (+)-fechado? (·)-fechado? (^)-fechado?
4. Na aula anterior mostrei um esboço para demonstrar o (BW) a partir do (MCT). Ache em uma outra maneira, a partir do (NIP).
5. Na aula anterior demonstramos o Θ. ϑ pequeno ⇒ (ϑⁿ)ₙ → 0. Ache uma outra demonstração, começando com a observação (justificada!) que $\frac 1 \vartheta = \delta + 1$ para algum $\delta > 0$. Use o teorema binomial! (Podemos mesmo?)

Prova 3.2

Em um universo paralelo

• Mais um toque de espaços métricos
• Mais um toque de teoria da medida e da integração
• Funções reais e seqüências de funções