fix bug

LorenzoLuccioli · Sep 10, 2024 · c56e7a1 · c56e7a1
1 parent 4a3f293
commit c56e7a1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/blueprint/src/sections/stat_div.tex b/blueprint/src/sections/stat_div.tex
@@ -152,7 +152,7 @@ \section{Statistical divergences}
 
 \begin{theorem}[Integral form of the statistical information]
   \label{thm:statInfo_eq_integral}
-  \lean{ProbabilityTheory.toReal_statInfo_eq_integral_max_of_le, ProbabilityTheory.toReal_statInfo_eq_integral_max_of_gt}
+  \lean{ProbabilityTheory.toReal_statInfo_eq_integral_max_of_le, ProbabilityTheory.toReal_statInfo_eq_integral_max_of_ge}
   \leanok
   \uses{def:statInfo}
   For finite measures $\mu, \nu$ and $\xi \in \mathcal M(\{0,1\})$,