Skip to content

Commit

Permalink
fix uses
Browse files Browse the repository at this point in the history
  • Loading branch information
RemyDegenne committed Mar 29, 2024
1 parent 65331ab commit 2f1092a
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions blueprint/src/sections/f_divergence.tex
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ \section{Data-processing inequality: sigma-algebras}
For $\mathcal A$ a sub-$\sigma$-algebra and $\mu$ a measure, we write $\mathcal \mu_{| \mathcal A}$ for the measure restricted to the $\sigma$-algebra.

\begin{lemma}
\label{thm:fDiv_trim_le_of_ac}
\label{lem:fDiv_trim_le_of_ac}
\lean{ProbabilityTheory.fDiv_trim_le_of_ac}
\leanok
\uses{def:fDiv}
Expand Down Expand Up @@ -222,7 +222,7 @@ \section{Data-processing inequality: sigma-algebras}
\end{theorem}

\begin{proof}
\uses{lem:fDiv_trim_le}
\uses{thm:fDiv_trim_le}
\end{proof}

\section{Conditional f-divergence}
Expand Down

0 comments on commit 2f1092a

Please sign in to comment.