added generated pdf and moved main.org -> aihe.org

1 files changed, 230 insertions, 0 deletions

diff --git a/aihe.org b/aihe.org
new file mode 100644
index 0000000..5465bfb
--- /dev/null
+++ b/aihe.org
@@ -0,0 +1,230 @@
+#+TITLE: Ääriarvojakaumien luokittelun formalisointi
+#+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: \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
+
+** Mitä on matematiikan tietokoneformalisointi?
+
+*** Text                                                              :BMCOL:
+:PROPERTIES:
+:BEAMER_col: .4
+:END:
+
+- <+-> Formaali kieli
+- <+-> Tyyppitarkistin
+- <+-> Tietokone vaatii jokaisen loogisen askeleen
+  
+*** Lean4 code                                                        :BMCOL:
+:PROPERTIES:
+:BEAMER_col: .6
+:END:
+
+#+NAME: leanexample
+#+begin_src lean4
+    variable (p q : Prop)
+    
+    lemma (h : p ∧ q) : q ∧ p :=
+      have hp : p := h.left
+      have hq : q := h.right
+      show q ∧ p from
+        And.intro hq hp
+#+end_src
+
+
+** Miksi?
+
+Formalisoinnin hyötyjä:
+- <+-> Tietokone vaatii jokaisen loogisen askeleen
+- <+-> Helpompi tarkastettavuus  
+- <+-> Huoleton automatisaatio
+
+  
+** Esimerkki automatisaatiosta
+
+Korollaarin 4.2 todistuksesta [cite:@kelomäki2025].
+
+Oletus:
+\begin{align*}
+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\).
+
+
+** 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)
+
+  l1, = pl(
+      0,
+      x1,
+      pdf1(a1),
+      "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Phi_\\alpha (x) $"
+  )
+
+  l2, = pl(
+      1,
+      x2,
+      pdf2(a2),
+      "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Psi_\\alpha (x) $"
+  )
+
+  l3, = pl(
+      2,
+      x3,
+      pdf3,
+      "$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Lambda (x) $"
+  )
+
+  for ax in axes:
+      ax.legend()
+
+  plt.savefig('plot.png')
+#+end_src
+
+#+RESULTS: plot-frechet
+
+#+ATTR_LATEX: :width 1.1\textwidth
+#+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
+
+** 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
+
+#+print_bibliography:
+
+
+* 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?