From 511242219affad271cabcdcbb100e1c22a915751 Mon Sep 17 00:00:00 2001
From: RemyDegenne <Remydegenne@gmail.com>
Date: Thu, 7 Mar 2024 16:20:28 +0100
Subject: [PATCH] blueprint: simple fDiv lemmas

---
 blueprint/src/sections/f_divergence.tex     | 39 +++++++++++++++++++++
 blueprint/src/sections/kl_divergence.tex    |  2 +-
 blueprint/src/sections/renyi_divergence.tex |  4 +--
 3 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/blueprint/src/sections/f_divergence.tex b/blueprint/src/sections/f_divergence.tex
index 452b18d1..78c4ae4a 100644
--- a/blueprint/src/sections/f_divergence.tex
+++ b/blueprint/src/sections/f_divergence.tex
@@ -38,6 +38,45 @@ \section{Definition and basic properties}
 $\frac{d \mu}{d \mu}(x) = 1$ almost everywhere and $f(1) = 0$.
 \end{proof}
 
+\begin{lemma}
+  \label{lem:fDiv_mul}
+  %\lean{}
+  %\leanok
+  \uses{def:fDiv}
+  For all $a \in \mathbb{R}$, $D_{a f}(\mu, \nu) = a D_{f}(\mu, \nu)$.
+\end{lemma}
+
+\begin{proof}
+Linearity of the integral.
+\end{proof}
+
+\begin{lemma}
+  \label{lem:fDiv_linear}
+  %\lean{}
+  %\leanok
+  \uses{def:fDiv}
+  For finite measures $\mu$ and $\nu$ with $\mu(\mathcal X) = \nu(\mathcal X)$, $D_{x - 1}(\mu, \nu) = 0$.
+\end{lemma}
+
+\begin{proof}
+Computation.
+\end{proof}
+
+\begin{lemma}
+  \label{lem:fDiv_add_linear}
+  %\lean{}
+  %\leanok
+  \uses{def:fDiv}
+  For finite measures $\mu$ and $\nu$ with $\mu(\mathcal X) = \nu(\mathcal X)$, for all $a \in \mathbb{R}$, $D_{f + a(x - 1)}(\mu, \nu) = D_{f}(\mu, \nu)$.
+\end{lemma}
+
+This means that we can always choose $f'(1) = 0$ if we want (and $f$ is differentiable at $1$).
+
+\begin{proof}
+\uses{lem:fDiv_add, lem:fDiv_mul, lem:fDiv_linear}
+Linearity (Lemmas~\ref{lem:fDiv_add} and~\ref{lem:fDiv_mul}), then Lemma~\ref{lem:fDiv_linear}.
+\end{proof}
+
 \section{Conditional f-divergence}
 
 \begin{lemma}
diff --git a/blueprint/src/sections/kl_divergence.tex b/blueprint/src/sections/kl_divergence.tex
index 494eee6c..307894f1 100644
--- a/blueprint/src/sections/kl_divergence.tex
+++ b/blueprint/src/sections/kl_divergence.tex
@@ -17,7 +17,7 @@ \chapter{Kullback-Leibler divergence}
   %\lean{}
   %\leanok
   \uses{def:KL, def:fDiv}
-  $\KL(\mu, \nu) = D_f(\mu, \nu)$ for $f: x \mapsto x \log x$ or $f: x \mapsto x \log x - x + 1$.
+  $\KL(\mu, \nu) = D_f(\mu, \nu)$ for $f: x \mapsto x \log x$ or, for probability measures, $f: x \mapsto x \log x - x + 1$.
 \end{lemma}
 
 \begin{proof}
diff --git a/blueprint/src/sections/renyi_divergence.tex b/blueprint/src/sections/renyi_divergence.tex
index ece8cd81..00687994 100644
--- a/blueprint/src/sections/renyi_divergence.tex
+++ b/blueprint/src/sections/renyi_divergence.tex
@@ -16,7 +16,7 @@ \chapter{Rényi divergences}
   %\lean{}
   %\leanok
   \uses{def:fDiv, def:Renyi}
-  $R_\alpha(\mu, \nu) = \frac{1}{\alpha - 1} \log (1 + (\alpha - 1) D_f(\nu, \mu))$ for $f : x \mapsto \frac{1}{\alpha - 1}(x^{\alpha} - \alpha x + \alpha - 1)$. It is thus a monotone transformation of a f-divergence.
+  $R_\alpha(\mu, \nu) = \frac{1}{\alpha - 1} \log (1 + (\alpha - 1) D_f(\nu, \mu))$ for $f : x \mapsto \frac{1}{\alpha - 1}(x^{\alpha} - 1)$, which is convex with $f(1)=0$. It is thus a monotone transformation of a f-divergence.
 
   TODO: use this for the definition?
 \end{lemma}
@@ -72,7 +72,7 @@ \chapter{Rényi divergences}
   %\lean{}
   %\leanok
   \uses{def:Renyi}
-  Let $\mu, \nu$ be two measures on $\mathcal X$. Let $n \in \mathbb{N}$ and write $\mu^{\otimes n}$ for the product measure on $\mathbb{R}^n$ of $n$ times $\mu$.
+  Let $\mu, \nu$ be two measures on $\mathcal X$. Let $n \in \mathbb{N}$ and write $\mu^{\otimes n}$ for the product measure on $\mathcal X^n$ of $n$ times $\mu$.
   Then $R_\alpha(\mu^{\otimes n}, \nu^{\otimes n}) = n R_\alpha(\mu, \nu)$.
 \end{corollary}