From 2115969c445f901d0a85cfb9a4d6b432ddf1e646 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Mon, 4 Nov 2024 09:49:15 +0100 Subject: [PATCH 1/4] add wald's lemma --- blueprint/src/sections/sequential.tex | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/blueprint/src/sections/sequential.tex b/blueprint/src/sections/sequential.tex index aa19cc5c..6b319584 100644 --- a/blueprint/src/sections/sequential.tex +++ b/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{} From 32294be9bb52eef85c62781575f0414738bb4e3d Mon Sep 17 00:00:00 2001 From: RemyDegenne Date: Wed, 15 Jan 2025 16:19:57 +0100 Subject: [PATCH 2/4] text about rn derivs --- blueprint/src/sections/rn_deriv.tex | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/blueprint/src/sections/rn_deriv.tex b/blueprint/src/sections/rn_deriv.tex index e3f3fe91..344b8ac9 100644 --- a/blueprint/src/sections/rn_deriv.tex +++ b/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} From 52aa72068ed26a7235834a42f8541a7b8b6e8f31 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 7 Mar 2025 16:10:28 +0100 Subject: [PATCH 3/4] fix a proof --- blueprint/src/sections/kernels.tex | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/blueprint/src/sections/kernels.tex b/blueprint/src/sections/kernels.tex index a2ac0d8e..d291a835 100644 --- a/blueprint/src/sections/kernels.tex +++ b/blueprint/src/sections/kernels.tex @@ -408,7 +408,8 @@ \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) \: . @@ -420,7 +421,8 @@ \section{Bayesian inverse of a kernel} $\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 +434,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 From 23f459168aa420e37892ede42e61c43e705acaa1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 7 Mar 2025 16:16:45 +0100 Subject: [PATCH 4/4] add remark --- blueprint/src/sections/kernels.tex | 2 ++ 1 file changed, 2 insertions(+) diff --git a/blueprint/src/sections/kernels.tex b/blueprint/src/sections/kernels.tex index d291a835..b0139c85 100644 --- a/blueprint/src/sections/kernels.tex +++ b/blueprint/src/sections/kernels.tex @@ -416,6 +416,8 @@ \section{Bayesian inverse of a kernel} \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)$.