1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
#+TITLE: Ääriarvojakaumien luokittelun formalisointi
#+SUBTITLE: Affiinit reaaliakselin muunnokset
#+AUTHOR: Joel Kronqvist
#+LANGUAGE: fi
#+startup: beamer
#+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: \usetheme{Copenhagen}
#+LaTeX_HEADER: \usepackage[finnish]{babel}
#+LaTeX_HEADER: \newcommand{\R}{\mathbb{R}}
#+LaTeX_HEADER: \renewcommand{\vec}[1]{\mathbf{#1}}
* Formalisointi
** Esimerkki
*** Text :BMCOL:
:PROPERTIES:
:BEAMER_col: .4
:END:
Sample text
- Sample item
- Second item
*** 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
* Ääriarvojakaumat
** Mitä ne ovat?
Matikkaselitystä
** Kertymäfunktiot
\begin{align*}
\Phi_\alpha (x) &:= \begin{cases}
0, & \text{kun}\ x \le 0, \\
\exp( -x^{-\alpha}), &\text{muutoin}, \\
\end{cases} \\
\Psi_\alpha (x) &:= \begin{cases}
\exp(-(-x)^\alpha), & \text{kun}\ x \le 0, \\
1, &\text{muutoin}, \\
\end{cases} \\
\Lambda(x) &:= \exp(-e^{-x}), x \in \R
\end{align*}
** Kuvaajat
#+name: plot-frechet
#+begin_src python :results output :file ./plot.png :exports results
import numpy as np
import matplotlib.pyplot as plt
fig, axes = plt.subplots(1, 3)
fig.set_size_inches(10, 4)
a1 = 3.0
a2 = 1.2
pl = lambda axi, x, f, lab: axes[axi].plot(x, np.vectorize(f)(x), label=lab)
pl(
0,
np.linspace(1e-6, 3, 500),
lambda x: a1*x**(-a1-1)*np.exp(-(x**(-a1))) if x > 0 else 0,
"$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Phi_\\alpha (x) $"
)
pl(
1,
np.linspace(-3, 1, 500),
lambda x: a2 * ((-x) ** (a2 - 1)) * np.exp(-1 * ((-x) ** a2)) if x < 0 else 0,
"$ \\frac{\\mathrm{d}}{\\mathrm{d} x} \\Psi_\\alpha (x) $"
)
pl(
2,
np.linspace(-5, 5, 500),
lambda x: np.exp(-x) * np.exp(-np.exp(-x)),
"$ \\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: Test caption
[[./plot.png]]
* Affiinit muunnokset
** Dia 1
Teksti 1
* TODO
** Nimi?
|
