Minor blueprint additions

blueprint/src/sections/kernels.tex

@@ -408,19 +408,23 @@ \section{Bayesian inverse of a kernel}
   %\lean{}
   %\leanok
   \uses{def:bayesInv}
-  Let $\mu \in \mathcal M(\mathcal X)$ and $\kappa : \mathcal X \rightsquigarrow \mathcal Y$ such that $\kappa_\mu^\dagger$ exists and there exists $\nu \in \mathcal M(\mathcal X)$ such that $\kappa_\mu^\dagger$. Then for $\mu$-almost all $x$ and $(\kappa \circ \mu)$-almost all $y$,
+  Let $\mu \in \mathcal M(\mathcal X)$ and $\kappa : \mathcal X \rightsquigarrow \mathcal Y$ such that $\kappa_\mu^\dagger$ exists and such that $\kappa(x) \ll \kappa \circ \mu$ almost surely.
+  Then for $\mu$-almost all $x$ and $(\kappa \circ \mu)$-almost all $y$,
   \begin{align*}
   \frac{d \kappa_\mu^\dagger(y)}{d \mu}(x) = \frac{d \kappa(x)}{d(\kappa \circ \mu)}(y)
   \: .
   \end{align*}
 \end{lemma}
 
+If $\mathcal{X}$ is countable, then we do have $\kappa(x) \ll \kappa \circ \mu$ almost surely.
+
 \begin{proof}%\leanok
 \uses{}
 $\mu$-almost all $x$ and $(\kappa \circ \mu)$-almost all $y$ is the same as $(\mu \times (\kappa \circ \mu))$-almost all $(x, y)$.
 It suffices to show that for all measurable sets of $\mathcal X \times \mathcal Y$, the integrals with respect to that product measure of the two sides of the equality on the set are equal. Furthermore, it is sufficient to show it for sets of the form $s \times t$ since those are a $\pi$-system.
 
-TODO: do we have $\kappa_\mu^\dagger(y) \ll \mu$ and $\kappa(x) \ll \kappa \circ \mu$ a.e.?
+Since $\kappa(x) \ll \kappa \circ \mu$ almost surely, we have $\mu \otimes \kappa \ll \mu \times (\kappa \circ \mu)$, hence $(\kappa \circ \mu) \otimes \kappa_\mu^\dagger \ll (\kappa \circ \mu) \times \mu$.
+We get that $\kappa_\mu^\dagger(y) \ll \mu$ almost surely.
 \begin{align*}
 \int_{x \in s, y \in t} \frac{d \kappa_\mu^\dagger(y)}{d \mu}(x) \partial (\mu \times (\kappa \circ \mu))
 &= \int_{y \in t} \int_{x \in s} \frac{d \kappa_\mu^\dagger(y)}{d \mu}(x) \partial \mu \partial (\kappa \circ \mu)
@@ -432,7 +436,7 @@ \section{Bayesian inverse of a kernel}
 \end{align*}
 
 \begin{align*}
-\int_{x \in s, y \in t} \frac{d \kappa(x)}{d(\kappa \circ \mu)}(y) \partial (\mu \otimes \kappa)
+\int_{x \in s, y \in t} \frac{d \kappa(x)}{d(\kappa \circ \mu)}(y) \partial (\mu \times (\kappa \circ \mu))
 &= \int_{x \in s} \int_{y \in t} \frac{d \kappa(x)}{d(\kappa \circ \mu)}(y) \partial (\kappa \circ \mu) \partial \mu
 \\
 &= \int_{x \in s} \kappa(x)(t) \partial \mu

blueprint/src/sections/rn_deriv.tex

@@ -1,9 +1,17 @@
 \chapter{Radon-Nikodym derivatives and disintegration}
 \label{app:rnDeriv}
 
+For $\mu$ and $\nu$ two $\sigma$-finite measures on a measurable space $\mathcal{X}$, we can decompose $\mu$ into $\frac{d \mu}{d \nu} \cdot \nu + \mu_{\perp \nu}$, where $\frac{d \mu}{d \nu}$ is a measurable function, unique $\nu$-a.e., and $\mu_{\perp \nu} \perp \nu$.
+
+If we then introduce two kernels $\kappa, \eta : \mathcal X \rightsquigarrow \mathcal Y$, we will want to compare the joint measures $\mu \otimes \kappa$ and $\nu \otimes \eta$, as well as the compositions $\kappa \circ \mu$ and $\eta \circ \nu$.
+
 
 \section{Kernel Radon-Nikodym derivative}
 
+In standard Borel spaces, we can define a Radon-Nikodym derivative for finite kernels.
+This is a measurable function $\frac{d \kappa}{d \eta} : \mathcal X \times \mathcal Y \to \mathbb{R}_{+, \infty}$ with $\kappa = \frac{d \kappa}{d \eta} \cdot \eta + \kappa_{\perp \eta}$, where for all $x$, $\kappa_{\perp \eta}(x) \perp \eta(x)$.
+The hypothesis that the spaces are standard Borel is used to ensure the measurability of the function on the product space.
+Taking for all $x$ the ratio $\frac{d \kappa(x)}{d \eta(x)}$ would give us measurable function $\mathcal Y \to \mathbb{R}_{+, \infty}$ for all $x \in \mathcal X$, but not necessarily a jointly measurable function.
 
 \begin{definition}
   \label{def:kernel_rnDeriv}
@@ -44,7 +52,6 @@ \section{Kernel Radon-Nikodym derivative}
 
 \section{Composition-product}
 
-
 \subsection{Absolute Continuity}
 
 \begin{lemma}

blueprint/src/sections/sequential.tex

@@ -13,6 +13,7 @@ \section{Sequential testing}
 \end{itemize}
 The idea is that a good estimator stops quickly with low risk.
 
+
 \begin{lemma}
   \label{lem:llr_filtration_nat}
   %\lean{}
@@ -27,6 +28,7 @@ \section{Sequential testing}
 By Lemma~\ref{lem:rnDeriv_map_eq_rnDeriv_trim}, $\frac{d \mu^{\otimes \mathbb{N}}_{| \mathcal F_n}}{d \nu^{\otimes \mathbb{N}}_{| \mathcal F_n}}(x) = \frac{d \pi_{[n]*}\mu^{\otimes \mathbb{N}}}{d \pi_{[n]*}\nu^{\otimes \mathbb{N}}}(\pi_{[n]}(x))$ a.s. . The pushforwards simplify: $\pi_{[n]*}\nu^{\otimes \mathbb{N}} = \nu^{\otimes n}$.
 \end{proof}
 
+
 \begin{lemma}
   \label{lem:llr_stopping_time}
   %\lean{}
@@ -50,19 +52,36 @@ \section{Sequential testing}
 
 \end{proof}
 
+
+\begin{lemma}
+  \label{lem:wald_equation}
+  %\lean{}
+  \notready
+  \uses{}
+  Let $\mu \in \mathcal P(\mathcal X)$ and let $(X_n)_{n \in \mathbb{N}}$ be $\mu$-integrable real random variables. Let $\tau$ be a random variable with value in $\mathbb{N}$.
+  Suppose that $\mu[X_n \mathbb{I}\{\tau \ge n\}] = \mu[X_n]\mu\{\tau \ge n\}$ for all $n \in \mathbb{N}$ and that $\sum_{n=1}^\infty \mu[|X_n| \mathbb{I}\{\tau \ge n\}] < \infty$. Then the sums $S_\tau = \sum_{n=1}^\tau X_n$ and $T_\tau = \sum_{n=1}^\tau \mu[X_n]$ are integrable and $\mu[S_\tau] = \mu[T_\tau]$. 
+\end{lemma}
+
+\begin{proof}%\leanok
+\uses{}
+
+\end{proof}
+
+
 \begin{theorem}
   \label{thm:kl_stopping_time}
   %\lean{}
   %\leanok
   \uses{def:KL}
-  For $\mu, \nu \in \mathcal P(\mathcal X)$, $\KL(\mu_\tau, \nu_\tau) = \mu[\tau] \KL(\mu, \nu)$.
+  For $\mu, \nu \in \mathcal P(\mathcal X)$, if $\tau$ has finite expectation then $\KL(\mu_\tau, \nu_\tau) = \mu[\tau] \KL(\mu, \nu)$.
 \end{theorem}
 
 \begin{proof}
-\uses{lem:llr_stopping_time}
+\uses{lem:llr_stopping_time,lem:wald_equation}
 TODO: need Wald's first identity.
 \end{proof}
 
+
 \begin{lemma}
   \label{lem:renyiMeasure_stopping_time}
   %\lean{}
@@ -75,6 +94,7 @@ \section{Sequential testing}
 This is a guess, I did not check it. TODO
 \end{proof}
 
+
 \begin{theorem}
   \label{thm:renyi_stopping_time}
   %\lean{}