added a lot, it is almost finished, oops

1 files changed, 139 insertions, 36 deletions

diff --git a/main.org b/main.org
index 071aaa0..5465bfb 100644
--- a/main.org
+++ b/main.org
@@ -2,30 +2,42 @@
 #+SUBTITLE: Affiinit reaaliakselin muunnokset
 #+AUTHOR: Joel Kronqvist
 #+LANGUAGE: fi
+#+bibliography: references.bib
+
 #+startup: beamer
+#+BEAMER_THEME: Copenhagen
 #+LaTeX_CLASS: beamer
 #+LaTeX_CLASS_OPTIONS: [bigger]
 #+OPTIONS: H:2
 #+LATEX_HEADER: \usepackage{fontspec}
 #+LaTeX_HEADER: \setmonofont[Scale=0.8]{DejaVu Sans Mono}
-#+LaTeX_HEADER: \usetheme{Copenhagen}
 #+LaTeX_HEADER: \usepackage[finnish]{babel}
 #+LaTeX_HEADER: \newcommand{\R}{\mathbb{R}}
+#+LaTeX_HEADER: \newcommand{\N}{\mathbb{N}}
+#+LaTeX_HEADER: \renewcommand{\to}{\rightarrow}
 #+LaTeX_HEADER: \renewcommand{\vec}[1]{\mathbf{#1}}
+#+LATEX_HEADER: \renewcommand{\sectionname}{Osio}
+#+LaTeX_HEADER: \AtBeginSection[]{\begin{frame}[plain]\sectionpage\end{frame}}
+
+
+* Linkki kalvoihin
+
+Esityksen kalvot ovat saatavilla osoitteesta [[https://cron4.fi/aihe.pdf][cron4.fi/aihe.pdf]] tai seuraavan QR-koodin kautta:
+[[./qr.png]]
+
 
 * Formalisointi
 
-** Esimerkki
+** Mitä on matematiikan tietokoneformalisointi?
 
 *** Text                                                              :BMCOL:
 :PROPERTIES:
 :BEAMER_col: .4
 :END:
 
-Sample text
-
-- Sample item
-- Second item
+- <+-> Formaali kieli
+- <+-> Tyyppitarkistin
+- <+-> Tietokone vaatii jokaisen loogisen askeleen
   
 *** Lean4 code                                                        :BMCOL:
 :PROPERTIES:
@@ -44,62 +56,110 @@ Sample text
 #+end_src
 
 
-* Ääriarvojakaumat
-
-** Mitä ne ovat?
-
-Matikkaselitystä
+** Miksi?
 
+Formalisoinnin hyötyjä:
+- <+-> Tietokone vaatii jokaisen loogisen askeleen
+- <+-> Helpompi tarkastettavuus  
+- <+-> Huoleton automatisaatio
 
-** Kertymäfunktiot
+  
+** Esimerkki automatisaatiosta
 
+Korollaarin 4.2 todistuksesta [cite:@kelomäki2025].
 
+Oletus:
 \begin{align*}
-  \Phi_\alpha (x) &:= \begin{cases}
-    0, & \text{kun}\ x \le 0, \\
-    \exp( -x^{-\alpha}), &\text{muutoin}, \\
-  \end{cases} \\
-  \Psi_\alpha (x) &:= \begin{cases}
-    \exp(-(-x)^\alpha), & \text{kun}\ x \le 0, \\
-    1, &\text{muutoin}, \\
-  \end{cases} \\
-  \Lambda(x) &:= \exp(-e^{-x}), x \in \R
+2 &> -\frac{1}{2} n + \frac{1}{2} h - \frac{1}{4} q - 1 \\
+2 &> 3 n - \frac{3}{2} h + q - \frac{5}{2} \\
+2 &> - \frac{9}{4} n + h - \frac{3}{4} q - \frac{1}{4}.
 \end{align*}
 
+Väite: \(n<39\).
 
-** Kuvaajat
+
+** Esimerkki automatisaatiosta
+
+#+begin_src lean4
+  import Mathlib.Analysis.Normed.Field.Lemmas
+  
+  def tA (n : ℚ) (h q : ℚ) : ℚ :=
+    (-1/2) * n + 1/2 * h - 1/4 * q - 1
+  
+  def tB (n : ℚ) (h q : ℚ) : ℚ :=
+    3 * n - 3/2 * h + q - 5/2
+  
+  def tC (n : ℚ) (h q : ℚ) : ℚ :=
+    (-9/4) * n + h - 3/4 * q - 1/4
+#+end_src
+
+
+** Esimerkki automatisaatiosta
+
+#+begin_src lean4
+  lemma corollary_4_2 (n h q : ℚ)
+    (htA : tA n h q < 2)
+    (htB : tB n h q < 2)
+    (htC : tC n h q < 2):
+    n <39:= by
+  rw [tA, tB, tC] at *
+  linarith
+#+end_src
+
+
+* Ääriarvojakaumat
+
+** Ääriarvojakauma
+
+- <+-> Olkoot \(X_i : i \in \N\) riippumattomia kertymäfunktion $F$
+  mukaisesti jakautuneita satunnaismuuttujia. \[ M_n := \max
+  \left\{X_i : i \le n\right\} \]
+- <+-> Mitä tapahtuu, kun
+  \(n\rightarrow\infty\)?
+- <+-> Lisätään sopivat siirto- ja skaalausjonot $a_n, b_n : \N \rightarrow
+  \R$ $\Rightarrow$ $(1 / a_n) M_n - b_n / a_n$ ja $F(a_n x + b_n)^n$ suppenevat.
+
+
+** Ääriarvojakaumien kuvaajat
 
 #+name: plot-frechet
 #+begin_src python :results output :file ./plot.png :exports results
   import numpy as np
   import matplotlib.pyplot as plt
+  import matplotlib.animation as animation
 
   fig, axes = plt.subplots(1, 3)
   fig.set_size_inches(10, 4)
 
   a1 = 3.0
   a2 = 1.2
+  x1 = np.linspace(1e-6, 3, 500)
+  x2 = np.linspace(-3, 1, 500)
+  x3 = np.linspace(-5, 5, 500)
+  pdf1 = lambda a1: lambda x: a1*x**(-a1-1)*np.exp(-(x**(-a1))) if x > 0 else 0
+  pdf2 = lambda a2: lambda x: a2 * ((-x) ** (a2 - 1)) * np.exp(-1 * ((-x) ** a2)) if x < 0 else 0
+  pdf3 = lambda x: np.exp(-x) * np.exp(-np.exp(-x))
 
   pl = lambda axi, x, f, lab: axes[axi].plot(x, np.vectorize(f)(x), label=lab)
 
-  pl(
+  l1, = pl(
       0,
-      np.linspace(1e-6, 3, 500),
-      lambda x: a1*x**(-a1-1)*np.exp(-(x**(-a1))) if x > 0 else 0,
+      x1,
+      pdf1(a1),
       "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Phi_\\alpha (x) $"
   )
 
-  pl(
+  l2, = pl(
       1,
-      np.linspace(-3, 1, 500),
-      lambda x: a2 * ((-x) ** (a2 - 1)) * np.exp(-1 * ((-x) ** a2)) if x < 0 else 0,
+      x2,
+      pdf2(a2),
       "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Psi_\\alpha (x) $"
   )
 
-  pl(
+  l3, = pl(
       2,
-      np.linspace(-5, 5, 500),
-      lambda x: np.exp(-x) * np.exp(-np.exp(-x)),
+      x3,
+      pdf3,
       "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Lambda (x) $"
   )
 
@@ -112,16 +172,59 @@ Matikkaselitystä
 #+RESULTS: plot-frechet
 
 #+ATTR_LATEX: :width 1.1\textwidth
-#+CAPTION: Test caption
+#+CAPTION: Esimerkit ääriarvojakaumien tiheysfunktioista
 [[./plot.png]]
 
 
+** Ääriarvojakaumien kertymäfunktiot
+
+
+\begin{align*}
+  \Phi_\alpha (x) &:= \begin{cases}
+    0, & \text{kun}\ x \le 0 \\
+    \exp( -x^{-\alpha}), &\text{muutoin} \\
+  \end{cases}\ (\alpha > 0), \\
+  \Psi_\alpha (x) &:= \begin{cases}
+    \exp(-(-x)^\alpha), & \text{kun}\ x \le 0 \\
+    1, &\text{muutoin} \\
+  \end{cases}\ (\alpha > 0), \\
+  \Lambda(x) &:= \exp(-e^{-x})
+\end{align*}
+
+
 * Affiinit muunnokset
 
-** Dia 1
+** Reaaliakselin affiini muunnos
+
+- Affiini muunnos koostuu siirrosta ja skaalauksesta
+- Reaaliakselin affiinit muunnokset ovat muotoa $f : \R \to \R, x
+  \mapsto a x + b$.
+- Suunnan säilyttäville affiineille muunnoksille $a > 0$.
+
+  
+** Luokittelutulos
+
+Olkoot kaikilla $s, t > 0, A_t (x) = a_t x + b_t, (a_t > 0)$ affiineja
+muunnoksia, joilla $A_{s t} = A_s \circ A_t$ ja $a$, $b$ mitallisia funktioita.
+
+- On olemassa $\beta \in \R$ jolla \(\forall t > 0, x \in \R :\)
+  \[ A_t(x) = x + \beta \log t \]
+  TAI
+- On olemassa $\rho \ne 0$ ja $c \in \R$ joilla kaikilla $t > 0, x \in \R$ pätee
+  \[ A_t(x) = t^\rho (x - c) + c \]
+
+
+* Lähteet
+
+** Lähteet ja viittaukset
 
-Teksti 1
+#+print_bibliography:
 
 
-* TODO
-** Nimi?
+* TODO [0/2]
+- [ ] Nimi?
+- [ ] Lisää kuva siirtodiasta affiinien muunnosten dioihin
+- [ ] todo a > 0
+- [ ] Muuta lean koodi (1.) tai kerro lisenssi
+- [ ] Lisää linkki PDF:ään
+- [ ] Laserosoitin?