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