path: root/aihe.org

#+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

#+ATTR_LATEX: :width 0.45\linewidth
#+CAPTION: Esityksen kalvot ovat saatavilla osoitteesta cron4.fi/aihe.pdf tai kuvan 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?