From 3fe43a1fb6d44b5b21bdc26bdabb1875ef7d530d Mon Sep 17 00:00:00 2001
From: RemyDegenne <Remydegenne@gmail.com>
Date: Sun, 24 Mar 2024 16:20:59 +0100
Subject: [PATCH] add leanok

---
 blueprint/src/sections/f_divergence.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/blueprint/src/sections/f_divergence.tex b/blueprint/src/sections/f_divergence.tex
index c2e09bc7..f9689946 100644
--- 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)$.