initial commit

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