fix blueprint proof of rho-increase

blueprint/src/chapter/further_improvement.tex

@@ -278,22 +278,24 @@ \section{Studying a minimizer}
   $$\rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i)\le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$
 \end{lemma}
 
-\begin{proof}\uses{rho-sums-sym, rho-cond-sym}
+\begin{proof}\uses{rho-sums-sym, rho-cond, rho-cond-sym, rho-cond-relabeled, cor-fibre}
   Let $T_1':=Y_3+Y_4$, $T_2':=Y_2+Y_4$.
   First note that
   \begin{align*}
     \rho(T_1|T_2,S)
-    &\le \rho(T_1|S) + \frac{1}{2}\bbI(T_1:T_2\mid S)  \textrm{ (by \Cref{rho-cond})}\\
-    &\le \frac{1}{2}(\rho(T_1)+\rho(T_1'))+\frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)) \textrm{ (by \Cref{rho-cond-sym})}\\
-    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)). \textrm{ (by \Cref{rho-sums-sym})}
+    &\le \rho(T_1|S) + \frac{1}{2}\bbI(T_1:T_2\mid S)  \\
+    &\le \frac{1}{2}(\rho(T_1)+\rho(T_1'))+\frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)) \\
+    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_2]+d[Y_3;Y_4]) + \frac{1}{2}(d[T_1;T_1']+\bbI(T_1:T_2\mid S)).
   \end{align*}
+  by \Cref{rho-cond}, \Cref{rho-cond-sym}, \Cref{rho-sums-sym} respectively.
   On the other hand, observe that
   \begin{align*}
     \rho(T_1|T_2,S)
-    &=\rho(Y_1+Y_2|T_2,T_2') \textrm{ (by \Cref{rho-cond-relabeled})}\\
-    &\le \frac{1}{2}(\rho(Y_1|T_2)+\rho(Y_2|T_2'))+\frac{1}{2}(d[Y_1|T_2;Y_2|T_2'])  \textrm{ (by \Cref{rho-sums-sym})}\\
-    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[Y_1|T_2;Y_2|T_2']). \textrm{ (by \Cref{rho-cond-sym})}.
+    &=\rho(Y_1+Y_2|T_2,T_2') \\
+    &\le \frac{1}{2}(\rho(Y_1|T_2)+\rho(Y_2|T_2'))+\frac{1}{2}(d[Y_1|T_2;Y_2|T_2'])  \\
+    &\le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[Y_1|T_2;Y_2|T_2']).
   \end{align*}
+  by \Cref{rho-cond-relabeled}, \Cref{rho-sums-sym}, \Cref{rho-cond-sym} respectively.
   By replacing $(Y_1,Y_2,Y_3,Y_4)$ with $(Y_1,Y_3,Y_2,Y_4)$ in the above inequalities, one has
   $$\rho(T_2|T_1,S) \le \frac{1}{4} \sum_{i} \rho(Y_i) +\frac{1}{4}(d[Y_1;Y_3]+d[Y_2;Y_4]) + \frac{1}{2}(d[T_2;T_2']+\bbI(T_1:T_2\mid S))$$
   and