fix checkdecls

blueprint/src/sections/f_divergence.tex

@@ -101,7 +101,7 @@ \section{Conditional f-divergence}
 
 \begin{definition}[Conditional f-divergence]
   \label{def:condFDiv}
-  \lean{ProbabilityTheory.condfDiv}
+  \lean{ProbabilityTheory.condFDiv}
   \leanok
   \uses{def:fDiv}
   Let $f : \mathbb{R} \to \mathbb{R}$, $\mu$ a measure on $\mathcal X$ and $\kappa, \eta : \mathcal X \rightsquigarrow \mathcal Y$ two Markov kernels from $\mathcal X$ to $\mathcal Y$. The conditional f-divergence between $\kappa$ and $\eta$ with respect to $\mu$ is

blueprint/src/sections/kl_divergence.tex

@@ -14,13 +14,13 @@ \chapter{Kullback-Leibler divergence}
 
 \begin{lemma}
   \label{lem:kl_eq_fDiv}
-  \lean{ProbabilityTheory.klReal_eq_fDivReal_mul_log}
+  \lean{ProbabilityTheory.klReal_eq_fDiv_mul_log}
   \leanok
   \uses{def:KL, def:fDiv}
   $\KL(\mu, \nu) = D_f(\mu, \nu)$ for $f: x \mapsto x \log x$.
 \end{lemma}
 
-\begin{proof} \leanok
+\begin{proof}
 Simple computation.
 \end{proof}
 

blueprint/src/sections/renyi_divergence.tex

@@ -2,7 +2,7 @@ \chapter{Rényi divergences}
 
 \begin{definition}[Rényi divergence]
   \label{def:Renyi}
-  \lean{ProbabilityTheory.renyiReal}
+  \lean{ProbabilityTheory.renyiDiv}
   \leanok
   \uses{def:KL}
   Let $\mu, \nu$ be two measures on $\mathcal X$. The Rényi divergence of order $\alpha \in [0,+\infty)$ between $\mu$ and $\nu$ is