From 39ec059f28b9a4be9c0d6e2798fc2bf465e8a4f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <remydegenne@gmail.com>
Date: Fri, 8 Mar 2024 17:20:59 +0100
Subject: [PATCH] blueprint: kl chain rule proof

---
 blueprint/src/sections/kl_divergence.tex | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/blueprint/src/sections/kl_divergence.tex b/blueprint/src/sections/kl_divergence.tex
index b4cfefec..1df6bc4f 100644
--- a/blueprint/src/sections/kl_divergence.tex
+++ b/blueprint/src/sections/kl_divergence.tex
@@ -40,6 +40,24 @@ \section{Chain rule and tensorization}
 \end{theorem}
 
 \begin{proof}
+\uses{lem:rnDeriv_compProd}
+Use Lemma~\ref{lem:rnDeriv_compProd} and Corollary~\ref{cor:rnDeriv_value} in a computation:
+\begin{align*}
+\KL(\mu \otimes \kappa, \nu \otimes \eta)
+&= \int_p \log \frac{d(\mu \otimes \kappa)}{d(\nu \otimes \eta)}(p) \partial (\mu \otimes \kappa)
+\\
+&= \int_x \int_y\log \left(\frac{d\mu}{d \nu}(x)\frac{d\kappa}{d \eta}(x,y)\right) \partial \kappa(x) \partial\mu
+\\
+&= \int_x \int_y\log \left(\frac{d\mu}{d \nu}(x)\right) + \log \left(\frac{d\kappa}{d \eta}(x,y)\right) \partial \kappa(x) \partial\mu
+\\
+&= \int_x \log \left(\frac{d\mu}{d \nu}(x)\right)\partial\mu + \int_y\log \left(\frac{d\kappa}{d \eta}(x,y)\right) \partial \kappa(x) \partial\mu
+\\
+&= \int_x \log \left(\frac{d\mu}{d \nu}(x)\right)\partial\mu + \int_y\log \left(\frac{d\kappa(x)}{d \eta(x)}(y)\right) \partial \kappa(x) \partial\mu
+\\
+&= \KL(\mu, \nu) + \KL(\kappa, \eta \mid \mu)
+\: .
+\end{align*}
+
 \end{proof}
 
 \begin{theorem}[Chain rule, product version]