add leanok

RemyDegenne · Mar 30, 2024 · 83b2c67 · 83b2c67
1 parent d543cdf
commit 83b2c67
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 16 deletions.
diff --git a/TestingLowerBounds/KullbackLeibler.lean b/TestingLowerBounds/KullbackLeibler.lean
@@ -18,21 +18,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 
 * `fooBar_unique`
 
-## Notation
-
-
-
-## Implementation details
-
-
-
-## References
-
-* [F. Bar, *Quuxes*][bibkey]
-
-## Tags
-
-Foobars, barfoos
 -/
 
 open Real MeasureTheory Filter

diff --git a/blueprint/src/sections/kl_divergence.tex b/blueprint/src/sections/kl_divergence.tex
@@ -20,7 +20,7 @@ \chapter{Kullback-Leibler divergence}
   $\KL(\mu, \nu) = D_f(\mu, \nu)$ for $f: x \mapsto x \log x$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
 Simple computation.
 \end{proof}