diff options
Diffstat (limited to 'main.org')
| -rw-r--r-- | main.org | 230 |
1 files changed, 0 insertions, 230 deletions
diff --git a/main.org b/main.org deleted file mode 100644 index 5465bfb..0000000 --- a/main.org +++ /dev/null @@ -1,230 +0,0 @@ -#+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? |