File size: 6,664 Bytes
63f41a6
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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
128
% common.sty -- single style for all 24 notes (series 01xx, 02xx, 03xx).
% Replaces common-m1/-m2/-m3 (kept as thin shims for old build logs; see STYLE_ALIGNMENT.md).
\ProvidesPackage{common}
\RequirePackage[margin=2.2cm]{geometry}
\RequirePackage[utf8]{inputenc}
\RequirePackage[T1]{fontenc}
\RequirePackage{amsmath,amssymb,amsthm,mathtools,bm}
\RequirePackage{booktabs,array,enumitem,longtable}
\RequirePackage[dvipsnames]{xcolor}
\RequirePackage[most]{tcolorbox}
\RequirePackage{listings}
\RequirePackage[hidelinks]{hyperref}
\RequirePackage{microtype}
\newcolumntype{P}[1]{>{\raggedright\arraybackslash}p{#1}}
\setlength{\emergencystretch}{3em}
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.55em}
\setlist{itemsep=2pt,topsep=3pt}
\renewcommand{\arraystretch}{1.15}
% ---- theorem-like environments ------------------------------------------
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\theoremstyle{remark}
\newtheorem*{remark}{Remark}
% ---- the house skeleton: problem -> notation -> derivation -> result -> what breaks -> next
\newtcolorbox{problem}{colback=gray!6,colframe=gray!60,title={The problem},
  fonttitle=\bfseries\small,boxrule=0.5pt,arc=1pt}
\newcommand{\question}[1]{\textbf{The question.} #1\par\smallskip}
\newtcolorbox{result}[1][Boxed result]{colback=Cerulean!6,colframe=Cerulean!70!black,
  boxrule=0.9pt,arc=2pt,title={#1},fonttitle=\bfseries\small}
\newtcolorbox{breaks}[1][]{colback=BrickRed!5,colframe=BrickRed!70!black,
  boxrule=0.6pt,arc=2pt,title={Failure modes and the assumption each one violates},
  fonttitle=\bfseries\small,#1}
\newcommand{\nextnote}[1]{\begin{tcolorbox}[colback=blue!4,colframe=blue!50!black,
  title={Next},fonttitle=\bfseries\small,boxrule=0.5pt,arc=1pt]#1\end{tcolorbox}}
\newcommand{\notehead}[3]{%
  {\raggedright\Large\bfseries Note #1 \,--\, #2}\\[2pt]
  {\raggedright\small\itshape #3\par}\vspace{2pt}\hrule\vspace{4pt}}
\newcommand{\nbref}[1]{\texttt{notebooks/#1}}
\newcommand{\ver}[1]{\textcolor{green!40!black}{\small[\textsf{verified}: #1]}}
% ---- shared notation ------------------------------------------------------
\DeclareMathOperator*{\argmax}{arg\,max}
\DeclareMathOperator*{\argmin}{arg\,min}
\DeclareMathOperator{\Var}{Var}
\DeclareMathOperator{\Cov}{Cov}
\DeclareMathOperator{\Bern}{Bern}
\DeclareMathOperator{\Bin}{Bin}
\DeclareMathOperator{\KL}{KL}
\DeclareMathOperator{\clip}{clip}
\DeclareMathOperator{\sg}{sg}
\DeclareMathOperator{\TV}{TV}
\DeclareMathOperator{\FV}{FV}
\DeclareMathOperator{\imax}{imax}
\newcommand{\ESS}{\mathrm{ESS}}
\newcommand{\E}{\mathbb{E}}
\renewcommand{\Pr}{\mathbb{P}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\ind}{\mathbb{1}}               % bare indicator symbol (02xx notes)
\newcommand{\indb}[1]{\mathbb{1}\!\left[#1\right]} % bracketed indicator (01xx notes)
\newcommand{\pa}{\pi_\theta}
\newcommand{\pth}{\pi_\theta}
\newcommand{\pold}{\pi_{\theta_{\mathrm{old}}}}
\newcommand{\score}{\nabla_\theta\log\pi_\theta}
\newcommand{\given}{\,\middle|\,}
\newcommand{\pk}{\mathrm{pass@}k}
\newcommand{\hatpk}{\widehat{\mathrm{pass@}k}}
% ---- formal-methods notation and Lean listings (03xx notes) ---------------
\newcommand{\Prop}{\mathsf{Prop}}
\newcommand{\Type}{\mathsf{Type}}
\newcommand{\Sort}{\mathsf{Sort}}
\newcommand{\bool}{\mathsf{Bool}}
\newcommand{\wpc}{\mathrm{wp}}
\newcommand{\hoare}[3]{\{#1\}\;#2\;\{#3\}}
\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\lean}[1]{\texttt{#1}}
% Lean listings (unicode-safe: declare the few glyphs we use)
\lstdefinelanguage{Lean}{
  morekeywords={theorem,lemma,def,example,by,fun,match,with,if,then,else,let,in,
    fun,intro,exact,apply,induction,cases,simp,omega,decide,rfl,have,show,from,
    inductive,structure,class,instance,where,open,import,namespace,axiom,partial,
    termination_by,decreasing_by,at,using,rw,unfold,split,rcases,obtain},
  sensitive=true, morecomment=[l]{--}, morestring=[b]"}
\lstset{language=Lean,basicstyle=\ttfamily\footnotesize,breaklines=true,
  columns=fullflexible,keepspaces=true,frame=single,rulecolor=\color{black!25},
  keywordstyle=\color{Blue}\bfseries,commentstyle=\color{OliveGreen}\itshape,
  xleftmargin=0.5em,xrightmargin=0.5em,aboveskip=0.4em,belowskip=0.2em,
  literate={→}{{$\to$}}1 {←}{{$\leftarrow$}}1 {↔}{{$\leftrightarrow$}}1
    {∀}{{$\forall$}}1 {∃}{{$\exists$}}1 {¬}{{$\neg$}}1 {∧}{{$\wedge$}}1 {∨}{{$\vee$}}1
    {≤}{{$\le$}}1 {≥}{{$\ge$}}1 {≠}{{$\ne$}}1 {ℕ}{{$\mathbb{N}$}}1 {ℤ}{{$\mathbb{Z}$}}1
    {ℝ}{{$\mathbb{R}$}}1 {λ}{{$\lambda$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1
    {α}{{$\alpha$}}1 {β}{{$\beta$}}1 {σ}{{$\sigma$}}1 {₀}{{$_0$}}1 {₁}{{$_1$}}1
    {₂}{{$_2$}}1 {₃}{{$_3$}}1 {∑}{{$\sum$}}1 {∣}{{$\mid$}}1 {×}{{$\times$}}1
    {⊥}{{$\bot$}}1 {∈}{{$\in$}}1 {∘}{{$\circ$}}1 {↑}{{$\uparrow$}}1 {·}{{$\cdot$}}1
    {≡}{{$\equiv$}}1 {⊢}{{$\vdash$}}1 {∅}{{$\emptyset$}}1 {∩}{{$\cap$}}1 {π}{{$\pi$}}1
    {⁻}{{$^-$}}1 {¹}{{$^1$}}1 {²}{{$^2$}}1 {ι}{{$\iota$}}1 {τ}{{$\tau$}}1 {Σ}{{$\Sigma$}}1 {Π}{{$\Pi$}}1 {⇒}{{$\Rightarrow$}}1 {⟹}{{$\Longrightarrow$}}1 {▸}{{$\triangleright$}}1 {⁅}{{[}}1 {≈}{{$\approx$}}1 {∘}{{$\circ$}}1}
% unicode that may appear in running text / \texttt
\DeclareUnicodeCharacter{2264}{\ensuremath{\le}}
\DeclareUnicodeCharacter{2265}{\ensuremath{\ge}}
\DeclareUnicodeCharacter{2260}{\ensuremath{\ne}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{2124}{\ensuremath{\mathbb{Z}}}
\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}
\DeclareUnicodeCharacter{2080}{\ensuremath{_0}}
\DeclareUnicodeCharacter{2081}{\ensuremath{_1}}
\DeclareUnicodeCharacter{2082}{\ensuremath{_2}}
\DeclareUnicodeCharacter{2083}{\ensuremath{_3}}
\DeclareUnicodeCharacter{2084}{\ensuremath{_4}}
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}
\DeclareUnicodeCharacter{2200}{\ensuremath{\forall}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\DeclareUnicodeCharacter{00B7}{\ensuremath{\cdot}}
\DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}
\DeclareUnicodeCharacter{2228}{\ensuremath{\vee}}
\DeclareUnicodeCharacter{2208}{\ensuremath{\in}}
\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}}
\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}}
\DeclareUnicodeCharacter{2223}{\ensuremath{\mid}}