added deletion of main.org (I forgor) and updated qr.png

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?