diff options
| -rw-r--r-- | aihe.org | 230 | ||||
| -rw-r--r-- | aihe.pdf | bin | 0 -> 426781 bytes |
2 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? diff --git a/aihe.pdf b/aihe.pdf Binary files differnew file mode 100644 index 0000000..d9d99f1 --- /dev/null +++ b/aihe.pdf |