add leanok

RemyDegenne · Mar 24, 2024 · 3fe43a1 · 3fe43a1
1 parent 6cdbdd5
commit 3fe43a1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/blueprint/src/sections/f_divergence.tex b/blueprint/src/sections/f_divergence.tex
@@ -246,8 +246,8 @@ \section{Data-processing inequality}
 
 \begin{theorem}[Marginals]
   \label{thm:fDiv_fst_le}
-  %\lean{}
-  %\leanok
+  \lean{ProbabilityTheory.fDiv_fst_le}
+  \leanok
   \uses{def:fDiv}
   Let $\mu$ and $\nu$ be two measures on $\mathcal X \times \mathcal Y$ where $\mathcal Y$ is standard Borel, and let $\mu_X, \nu_X$ be their marginals on $\mathcal X$.
   Then $D_f(\mu_X, \nu_X) \le D_f(\mu, \nu)$.