Merge pull request RemyDegenne#150 from RemyDegenne/blueprint

Blueprint: mark the two main `sorry` as `\notready`

blueprint/src/macros/print.tex

@@ -12,8 +12,10 @@
 
 % Dummy macros that make sense only for web version.
 \newcommand{\lean}[1]{}
+\newcommand{\discussion}[1]{}
 \newcommand{\leanok}{}
 \newcommand{\mathlibok}{}
+\newcommand{\notready}{}
 % Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
 % latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
 % It uses LaTeX3 programming, this is why we use the expl3 package.

blueprint/src/sections/convex.tex

@@ -28,8 +28,9 @@ \chapter{Convex functions of Radon-Nikodym derivatives}
   %\lean{}
   %\leanok
   %\uses{}
+  \notready
   For $f$ convex, $f\left(\mu [g \mid m]\right) \le \mu [f \circ g \mid m]$.
 \end{theorem}
 
-\begin{proof}
+\begin{proof} %\leanok
 \end{proof}

blueprint/src/sections/dpi_div.tex

@@ -7,6 +7,8 @@
 
 Another important concept is the \emph{conditional divergence} of two kernels $\kappa, \eta : \mathcal X \rightsquigarrow \mathcal Y$ given a measure $\mu \in \mathcal M(\mathcal X)$. This is the value $D(\mu \otimes \kappa, \mu \otimes \eta)$.
 
+TODO: two possible concepts of conditional divergence are $D(\mu \otimes \kappa, \mu \otimes \eta)$ and $\mu\left[x \mapsto D(\kappa(x), \eta(x))\right]$. They are equal for $f$-divergences (which gives also convexity of the divergence) but not in general. 
+
 \section{Generic divergences}
 
 \begin{definition}[Divergence]

blueprint/src/sections/f_divergence.tex

@@ -578,6 +578,24 @@ \subsection{Integral representation of $f$-divergences}
 \end{proof}
 
 
+\begin{theorem}
+  \label{thm:integration_by_parts}
+  %\lean{}
+  %\leanok
+  \notready
+  \uses{}
+  If $f$ and $g$ are two Stieltjes functions with associated measures $\mu_f$ and $\mu_g$ and $f$ is continuous on $[a, b]$, then
+  \begin{align*}
+  \int_x f(x) \partial\mu_g = f(b)g(b) - f(a)g(a) - \int_x g(x) \partial\mu_f \: .
+  \end{align*}
+\end{theorem}
+
+\begin{proof} \notready
+\uses{}
+
+\end{proof}
+
+
 \begin{lemma}
   \label{lem:convex_taylor}
   \lean{ConvexOn.convex_taylor}
@@ -592,13 +610,13 @@ \subsection{Integral representation of $f$-divergences}
 \end{lemma}
 
 \begin{proof}\leanok
-\uses{}
+\uses{thm:integration_by_parts}
 Let $\Lambda$ be the Lebesgue measure and let $x < y$. Since $f$ has right derivative $f'_+$ in $(x,y)$ and $f'_+$ is integrable on that interval,
 \begin{align*}
 f(y) - f(x) = \int_{z \in (x, y]} f'_+(z) \partial \Lambda
 \: .
 \end{align*}
-We now integrate by parts, using Theorem TODO. $\Lambda$ is the measure obtained from the Stieltjes function $z \mapsto z - y$.
+We now integrate by parts, using Theorem~\ref{thm:integration_by_parts}. $\Lambda$ is the measure obtained from the Stieltjes function $z \mapsto z - y$.
 \begin{align*}
 \int_{z \in (x, y]} f'_+(z) \partial \Lambda
 &= - \int_{z \in (x,y]} (z - y)\partial \gamma_f + f'_+(y)(y - y) - f'_+(x)(x - y)
@@ -928,7 +946,7 @@ \subsubsection{Sigma-algebras}
 \end{lemma}
 
 \begin{proof}%\leanok
-\uses{lem:fDiv_map_eq_fDiv_trim_of_ac}
+\uses{lem:fDiv_map_eq_fDiv_trim_of_ac, thm:fDiv_trim_le}
 By Lemma~\ref{lem:fDiv_map_eq_fDiv_trim_of_ac},  $D_f(g_* \mu, g_* \nu) = D_f(\mu_{| g^* \mathcal Y}, \nu_{| g^* \mathcal Y})$. Then apply Theorem~\ref{thm:fDiv_trim_le}.
 \end{proof}
 

blueprint/src/sections/risk.tex

@@ -528,8 +528,6 @@ \subsection{Bayes risk increase}
 
 \section{Simple binary hypothesis testing}
 
-TODO: rework this section to use the Bayes risk increase?
-
 In this section, for a measure $\xi$ on $\{0,1\}$, we write $\xi_0$ for $\xi(\{0\})$ and $\xi_1$ for $\xi(\{1\})$~. We sometimes write $(a,b)$ for the measure $\xi$ on $\{0,1\}$ with $\xi_0 = a$ and $\xi_1 = b$.
 
 \begin{lemma}