blob: b940e2ed323249a2404f1cdc4a6d64b2573bdf5b (
plain)
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
|
#+TITLE: Formalizing the Classification of Extreme Value Distributions
#+SUBTITLE: One-parameter subgroups of Affine transformations
#+AUTHOR: Joel Kronqvist
#+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}
* Formalization
** First slide of formalization
*** 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
# \begin{minted}[autogobble, bgcolor=codebg, fontsize=\footnotesize, bgcolorpadding=2pt]{lean4}
* Extreme value distributions
** Fréchet
#+name: plot-frechet
#+begin_src python :results file link :file "frechet-plot.png" :exports results
import numpy as np
import matplotlib.pyplot as plt
a = 2.0 # α > 0 (shape/dispersion parameter)
x = np.linspace(1e-6, 5, 500)
pdf = np.vectorize(lambda x: a*x**(-a-1)*np.exp(-x**(-a)) if x > 0 else 0)(x)
plt.plot(x, pdf, lw=2, color='steelblue')
plt.savefig('frechet-plot.png')
#+end_src
#+RESULTS: plot-frechet
[[file:frechet-plot.png]]
** Gumbel
** Weibull
* Affine transformations
** This is slide 1 on affine transformations
Maybe add several slides to each category?
|
