Notes added from 042420 meeting.

sop.tex

@@ -189,7 +189,9 @@ We rewrite equation \eqref{eq:sig-j-last} in terms of $\dist$ distinct worlds, w
 The functions $\surj, \surj'$ are used to produce the mapping $\left(\wElem_1,\ldots, \wElem_{\prodsize}\right) \mapsto \left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)$.  Observe that the cartesian product of world values assigned to $\wElem_1,\ldots,\wElem_\prodsize$ throughout the summation can be rearranged into groups of world variables with distinct world values, for each distinct element $\dist$ in the set $[\prodsize]$.  For each $\dist \in [\prodsize]$, all possible combinations of $\dist$ world values is equivalently modeled by taking the set of surjective functions $\surj:[\prodsize]\mapsto [\dist]$ and using that set to obtain all respctive mappings $\left(\wElem_1,\ldots, \wElem_{\prodsize}\right) \mapsto \left(\dw_1,\ldots, \dw_{\prodsize}\right)$.
 For any $\dist$, the set of surjective mappings $\surj$ covers all unique mappings.
 
-Let us define the set $S_1 = \{\left(\wElem_1,\ldots, \wElem_{\prodsize}\right)~|~ \wElem_1,\ldots, \wElem_{\prodsize} \in \wSet, |\{\wElem_i ~|~ \forall i \in [\prodsize]\}| = \dist\}$.  Further define 
+Let us define the set 
+\[S_1 = \{\left(\wElem_1,\ldots, \wElem_{\prodsize}\right)~|~ \wElem_1,\ldots, \wElem_{\prodsize} \in \wSet, |\{\wElem_i ~|~ \forall i \in [\prodsize]\}| = \dist\}\].  Further define 
+\AH{change this to match the whiteboard from last time}
 \[S_2 = \left\{\left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)~|~ \left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right) \in \left\{\surj, \left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)~|~ \surj:[\prodsize] \mapsto [\dist], \dw_1 \prec \cdots \prec \dw_{\dist}\right\}\right\}.\]
 To prove that \cref{eq:sig-j-last} and \cref{eq:sig-j-distinct} are the same, we need to show that the following lemmas are true.
 \begin{Lemma}
@@ -197,7 +199,8 @@ The set $S_1$ is equal to the set $S_2$.
 \end{Lemma}
 \begin{proof}
 Note that $S_1 = S_2$ is the same as $S_1 \subseteq S_2 \wedge S_2 \subseteq S_1$.
-First, we argue that $S_2 \subseteq S_1$.  This follows by definition of $S_2$, since every tuple in the set has $\dist$ distinct worlds.  Next, we argue that $S_1 \subseteq S_2$.  Pick an arbitrary tuple $\left(\wElem_1,\ldots, \wElem_{\prodsize}\right)$ in $S_1$.  Note that it has $\dist$ distinct world values by definition of $S_1$. Name these $\dw_1,\ldots,\dw_{\dist}$ s.t. they respect $\prec$. Then the corresponding definition of $\surj$ follows from which $\dw_j$ each $\wElem_i$ maps to.
+First, we argue that $S_2 \subseteq S_1$.  This follows by definition of $S_2$, since every tuple in the set has $\dist$ distinct worlds.  \AH{add more explanation}
+Next, we argue that $S_1 \subseteq S_2$.  Pick an arbitrary tuple $\left(\wElem_1,\ldots, \wElem_{\prodsize}\right)$ in $S_1$.  Note that it has $\dist$ distinct world values by definition of $S_1$. Name these $\dw_1,\ldots,\dw_{\dist}$ s.t. they respect $\prec$. Then the corresponding definition of $\surj$ follows from which $\dw_j$ each $\wElem_i$ maps to.
 \end{proof}
 \begin{Lemma}
 $S_2$ is a valid set, i.e., given a distinct $\dw_1 \prec \cdots \prec \dw_{\dist}$ over every distinct $\surj:[\prodsize]\mapsto [\dist]$, the tuples $\left(\dw_{\surj(1)},\ldots, \dw_{\surj(\prodsize)}\right)$ are distinct.
@@ -231,7 +234,8 @@ Functions $\surj:[\prodsize]\mapsto [\dist], \surj':[\prodsize]\mapsto [\dist']$
 	\end{enumerate}
 \end{Definition}
 
-
+\AH{handle $\term_1$ first, then use the lemma to tackle eq 95; use lemma that was stated in terms of $\term_1$, and create another lemma for 95}
+\AH{explicity note the independence of h and s, to justify pushing expectations through products}
 \begin{Lemma}\label{lem:sig-j-survive}
 When $\surj, \surj'$are matching, where $\forall j \in[\dist], \dw_{_j} = \dw_{'_j}$, \cref{eq:sig-j-distinct} is exactly 
 \[
@@ -284,6 +288,7 @@ Further see how the requirement that $\dw_i = \dw'_i$ gives us the precise combi
 
 To prove that \cref{lem:sig-j-survive} is true, consider what the expectation looks like when $\surj, \surj'$ are not matching.  The first condition for $\surj, \surj'$ to be matching is violated when $\dist \neq \dist'$.  
 \AH{The following observation isn't necessary to complete the proof.  I'll just leave it for now in case it may be valuable down the road.}
+\AH{Don't use $\exists, \forall$ in prose; mathematcial notation shouldn't be used to replace the prose, only to enhance the prose.}
 Observe that $\forall \dist \in [\prodsize], \sum_{i = 1}^{\dist}|\surj^{-1}(i)| = \prodsize$ and that this fact implies for $\dist, \dist' \in [\prodsize] ~|~\dist \neq \dist', \exists i \in [m] ~|~\forall j \in [m], \surj^{-1}(i)| \neq |\surj'^{-1}(j)|$, meaning that if we have that $\dist \neq \dist'$, then the second matching condition is also violated.  
 \AH{Moving on...}Note that $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_{\dist'}'$ are distinct world values such that $\forall i \neq j \in [\dist], \dw_i = \dw_i' \neq \dw_j = \dw_j'$.  To make things easier, assume that $\dist < \dist'$.  The opposite case of $\dist > \dist'$ has a symmetrical proof.  Fixing variables $\dw_1\ldots\dw_\dist, \dw_1'\ldots\dw_\dist$, we have at least one $\dw_i$ without a conjugate, and at least one extra distinct value, $\dw_{\dist'}'$, for which no $\dw_{\dist'}$ exists.  This (these) distinct term(s) cancel(s) out all the other values in the expectations.