diff options
| -rw-r--r-- | main.org | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/main.org b/main.org new file mode 100644 index 0000000..b940e2e --- /dev/null +++ b/main.org @@ -0,0 +1,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? + |